mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
⊢ Group α

Tactic:
apply e.injective.group _ <;> intros

Goal state after:
case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ e 1 = 1

case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

case inv
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ : α
⊢ e x✝⁻¹ = (e x✝)⁻¹

case div
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ y✝ : α
⊢ e (x✝ / y✝) = e x✝ / e y✝

case npow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ : α
n✝ : ℕ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝

case zpow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ : α
n✝ : ℤ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
⊢ atTop = comap Subtype.val atTop

Tactic:
← map_val_Ici_atTop a,

Goal state after:
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
⊢ atTop = comap Subtype.val (map Subtype.val atTop)
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x ↦ f ↑x) atTop l ↔ Tendsto f atTop l

Tactic:
← map_val_Ici_atTop a,

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x ↦ f ↑x) atTop l ↔ Tendsto f (map Subtype.val atTop) l
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x : α
⊢ IsCofinal {x} ↔ IsTop x

Tactic:
simp [IsCofinal, IsTop]

Goal state after:
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ a • b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
by
  rw [← neg_nonneg, ← smul_neg, smul_nonneg_iff, neg_nonneg, neg_nonpos]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
M : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
A : Type u_3
inst✝⁴ : Semiring A
inst✝³ : Module R A
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
S : Submodule A M
inst✝ : Module.Finite R A
hS : Module.Finite A ↥S
⊢ Module.Finite R ↥(Submodule.restrictScalars R S)

Tactic:
exact Module.Finite.trans A S

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : (g.comp f).Finite
⊢ g.Finite

Tactic:
algebraize [f, g, g.comp f]
  exact .of_restrictScalars_finite A B C

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hf : IsNormal f
⊢ DirSupClosed (range f)

Tactic:
intro s hs hs₀ _ a ha
  have hf' : (f ⁻¹' s).Nonempty := by
    obtain ⟨b, hb⟩ := hs₀
    obtain ⟨c, rfl⟩ := hs hb
    exact ⟨c, hb⟩
  have : Nonempty α := ⟨a⟩
  let := WellFoundedLT.toOrderBot α
  let := WellFoundedLT.conditionallyCompleteLinearOrderBot α
  have hfl : IsLUB (f ⁻¹' s) (sSup (f ⁻¹' s)) :=
    isLUB_csSup hf' ⟨a, fun b hb ↦ hf.strictMono.le_apply.trans (ha.1 hb)⟩
  have ha' := hf.map_isLUB hfl hf'
  rw [image_preimage_eq_of_subset hs] at ha'
  obtain rfl := ha.unique ha'
  exact mem_range_self _

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: case mp
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
a : Ordinal.{u}
e : liftInitialSeg.toRelEmbedding a = type s
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ liftInitialSeg.toRelEmbedding (type r) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})

Tactic:
exact lift_type_lt.{u, u + 1, max (u + 1) v}.2 ⟨typein r⟩

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a✝ b : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝³ : IsWellOrder α r
β : Type u
s : β → β → Prop
x✝² : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
x✝¹ : IsWellOrder γ t
x✝ : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), f (Sum.inl a) = Sum.inl a
a : α
x : γ ⊕ β
hx : f (Sum.inr a) = x
⊢ ∃ b, x = Sum.inr b

Tactic:
obtain x | x := x

Goal state after:
case inl
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a✝ b : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝³ : IsWellOrder α r
β : Type u
s : β → β → Prop
x✝² : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
x✝¹ : IsWellOrder γ t
x✝ : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), f (Sum.inl a) = Sum.inl a
a : α
x : γ
hx : f (Sum.inr a) = Sum.inl x
⊢ ∃ b, Sum.inl x = Sum.inr b

case inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a✝ b : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝³ : IsWellOrder α r
β : Type u
s : β → β → Prop
x✝² : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
x✝¹ : IsWellOrder γ t
x✝ : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), f (Sum.inl a) = Sum.inl a
a : α
x : β
hx : f (Sum.inr a) = Sum.inr x
⊢ ∃ b, Sum.inr x = Sum.inr b
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case neg
β : Type u_3
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : ¬BddAbove (range f)
⊢ ⨆ i, f i + 1 ≤ ⨆ i, f i

Tactic:
· rw [ciSup_of_not_bddAbove hf', ciSup_of_not_bddAbove]
    rwa [← bddAbove_range_add_one_iff] at hf'

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case succ
n : ℕ
IH : ↑n ≤ (↑n).ord
⊢ ↑(n + 1) ≤ (↑(n + 1)).ord

Tactic:
| succ n IH =>

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.inl
b n : ℕ
hb : 1 < b
h : n < b
⊢ log b 0 = log b n - 1

Tactic:
log_of_lt h,

Goal state after:
case inr.inl
b n : ℕ
hb : 1 < b
h : n < b
⊢ log b 0 = 0 - 1
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case succ
a : Ordinal.{u_1}
n : ℕ
IH : a ^ ↑n = a ^ n
⊢ a ^ ↑(n + 1) = a ^ (n + 1)

Tactic:
| succ n IH =>

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b c : Ordinal.{u_1}
ab : a < b
⊢ a ^ succ c < b ^ succ c

Tactic:
rw [opow_succ, opow_succ]
  exact mul_lt_mul_of_le_of_lt_of_nonneg_of_pos (by gcongr) ab zero_le (opow_pos _ ab.bot_lt)

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case case1.inr
b : ℕ
hb : 1 < b
x y : ℕ
h : 1 < b ∧ 1 < x
H₁ : b ^ (clog.go x b x).snd < x
H₂ : x ≤ b ^ ((clog.go x b x).snd + 1)
hy : (clog.go x b x).snd ≥ y
⊢ (clog.go x b x).snd + 1 ≤ y ↔ x ≤ b ^ y

Tactic:
| inr hy =>

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl
b x y : ℕ
h : x ≤ b ^ y
hb : 1 < b
⊢ clog b x ≤ y

Tactic:
rwa [clog_le_iff_le_pow hb]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case refine_1
a : Ordinal.{u}
⊢ nfp (fun x ↦ a + x) 0 = a * ω

Tactic:
exact nfp_add_zero a

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ IsInitial 0

Tactic:
exact_mod_cast isInitial_natCast 0

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case succ
n : ℕ
IH : preOmega ↑n = ↑n
⊢ preOmega ↑(n + 1) = ↑(n + 1)

Tactic:
| succ n IH =>

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inr.inl
a : Ordinal.{u}
h✝ : 0 < a
hb₁ : 0 ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) 0
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (a * 0)

pp: case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
h✝ : 0 < a
hb₁' : 0 < b
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (a * b)

Tactic:
· rw [mul_zero]
      exact isPrincipal_zero

Goal state after:
case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
h✝ : 0 < a
hb₁' : 0 < b
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (a * b)
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case refine_2
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
⊢ (fun x1 x2 ↦ x1 * x2) a b < o

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Goal state after:
case refine_2.inl
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
b : Ordinal.{u}
hbo : b < o
hao : 0 < o
⊢ (fun x1 x2 ↦ x1 * x2) 0 b < o

case refine_2.inr
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
ha : a ≠ 0
⊢ (fun x1 x2 ↦ x1 * x2) a b < o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case neg.inr.inr
n : ℕ
h2a : ¬↑n = 0
m : ℕ
hb : ↑m ≠ 0
h : ↑n * ↑m = ↑n
⊢ ↑m = 1

Tactic:
← Ne

Goal state after:
case neg.inr.inr
n : ℕ
h2a : ↑n ≠ 0
m : ℕ
hb : ↑m ≠ 0
h : ↑n * ↑m = ↑n
⊢ ↑m = 1
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: a : Ordinal.{u_1}
f : ↑(Iio a) → Ordinal.{u_1}
hf : StrictMono f
ha : IsSuccPrelimit a
⊢ (⨆ i, f i).cof = a.cof

Tactic:
rw [← iSup_Iio_add_one hf ha, cof_iSup_Iio_add_one hf]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ ℶ_ ↑n ≤ lift.{v, u} c ↔ ℶ_ ↑n ≤ c

Tactic:
by
  simpa using lift_le (a := ℶ_ n)

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case add_one
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
a✝ : a + 1 = a → (a + 1).cof ≤ (f (a + 1)).cof
⊢ (f (a + 1)).cof ≠ 0

Tactic:
cof_eq_zero.ne

Goal state after:
case add_one
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
a✝ : a + 1 = a → (a + 1).cof ≤ (f (a + 1)).cof
⊢ f (a + 1) ≠ 0
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v}
c : Ordinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), f i < c
⊢ lsub f < c

Tactic:
apply lift_iSup_add_one_lt_of_lt_cof _ hf

Goal state after:
ι : Type u
f : ι → Ordinal.{max u v}
c : Ordinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), f i < c
⊢ Cardinal.lift.{max u v, u} #ι < (lift.{u, max u v} c).cof
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u_1}
H : ∀ (i : ι), f i < iSup f
⊢ (iSup f).cof ≤ #ι

Tactic:
by
  by_contra! hf
  exact (iSup_lt_of_lt_cof hf H).false

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
⊢ (a ^ b).card = max a.card b.card

Tactic:
apply (card_opow_le_of_omega0_le_right a hb).antisymm (max_le _ _) <;> apply card_le_card

Goal state after:
a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
⊢ a ≤ a ^ b

a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
⊢ b ≤ a ^ b
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hf : ∀ (i : ι), f i < c.ord
⊢ lsub f < c.ord

Tactic:
apply lift_iSup_add_one_lt_of_lt_cof _ hf

Goal state after:
ι : Type u
f : ι → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hf : ∀ (i : ι), f i < c.ord
⊢ lift.{max u v, u} #ι < (Ordinal.lift.{u, max u v} c.ord).cof
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
e₁ : lift.{max u v, u} #(α ≃ α) = #(α ≃ β')
e₂ : lift.{max u v, u} #(α → α) = #(α → β')
⊢ #(α ≃ β') = #(α → β')

Tactic:
← e₁,

Goal state after:
α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
e₁ : lift.{max u v, u} #(α ≃ α) = #(α ≃ β')
e₂ : lift.{max u v, u} #(α → α) = #(α → β')
⊢ lift.{max u v, u} #(α ≃ α) = #(α → β')
Module: Mathlib.Data.DFinsupp.Submonoid

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddZeroClass (β i)
inst✝² : AddCommMonoid γ
S : Type u_1
inst✝¹ : SetLike S γ
inst✝ : AddSubmonoidClass S γ
s : S
f : Π₀ (i : ι), β i
g : (i : ι) → β i →+ γ
h : ∀ (c : ι), f c ≠ 0 → (g c) (f c) ∈ s
⊢ (sumAddHom g) f ∈ s

Tactic:
rw [DFinsupp.sumAddHom_apply]
    exact dfinsuppSum_mem s f (g ·) h

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Reflection

Goal state before:
pp: α : Type u_1
n : ℕ
P : (Fin n.succ → α) → Prop
⊢ Forall P ↔ ∀ (x : Fin n.succ → α), P x

Tactic:
by simp only [Forall, forall_iff, Fin.forall_fin_succ_pi, Matrix.vecCons]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case refine_1
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝¹ : (i : ι) → AddCommMonoid (β₁ i)
inst✝ : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → β₁ i →+ β₂ i
x : Π₀ (i : ι), β₂ i
x✝ : x ∈ AddMonoidHom.mrange (mapRange.addMonoidHom f)
i : ι
hi : i ∈ Set.univ
y : Π₀ (i : ι), β₁ i
hy : (mapRange.addMonoidHom f) y = x
⊢ x i ∈ (fun i ↦ ((fun i ↦ AddMonoidHom.mrange (f i)) i).carrier) i

pp: case refine_2
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝¹ : (i : ι) → AddCommMonoid (β₁ i)
inst✝ : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → β₁ i →+ β₂ i
x : Π₀ (i : ι), β₂ i
h : ⇑x ∈ AddSubmonoid.pi Set.univ fun i ↦ AddMonoidHom.mrange (f i)
⊢ x ∈ AddMonoidHom.mrange (mapRange.addMonoidHom f)

Tactic:
· simp [← hy]

Goal state after:
case refine_2
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝¹ : (i : ι) → AddCommMonoid (β₁ i)
inst✝ : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → β₁ i →+ β₂ i
x : Π₀ (i : ι), β₂ i
h : ⇑x ∈ AddSubmonoid.pi Set.univ fun i ↦ AddMonoidHom.mrange (f i)
⊢ x ∈ AddMonoidHom.mrange (mapRange.addMonoidHom f)
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : iSupIndep p
⊢ Function.Injective ⇑((lsum ℕ) fun i ↦ (p i).subtype)

Tactic:
rw [iSupIndep_iff_forall_dfinsupp] at h

Goal state after:
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x → x = 0
⊢ Function.Injective ⇑((lsum ℕ) fun i ↦ (p i).subtype)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case h.insert
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (span R (f i)) (⨆ i ∈ t, span R (f i))
i : ι
s : Finset ι
his : i ∉ s
ih : LinearIndepOn R id (⋃ i ∈ s, f i)
⊢ LinearIndepOn R id (⋃ i_1 ∈ insert i s, f i_1)

Tactic:
Finset.set_biUnion_insert

Goal state after:
case h.insert
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (span R (f i)) (⨆ i ∈ t, span R (f i))
i : ι
s : Finset ι
his : i ∉ s
ih : LinearIndepOn R id (⋃ i ∈ s, f i)
⊢ LinearIndepOn R id (f i ∪ ⋃ x ∈ s, f x)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case right
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : f ∈ Finsupp.supported R R J
sum_f : f i • v i = -∑ x ∈ f.support.erase i, f x • v x
f_ne : f ≠ 0
hfi : f i ≠ 0
hfi' : i ∈ f.support
⊢ -∑ x ∈ f.support.erase i, f x • v x ∈ span R (v '' I)

Tactic:
refine neg_mem (sum_mem fun c hc => smul_mem _ _ (subset_span ⟨c, ?_, rfl⟩))

Goal state after:
case right
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : f ∈ Finsupp.supported R R J
sum_f : f i • v i = -∑ x ∈ f.support.erase i, f x • v x
f_ne : f ≠ 0
hfi : f i ≠ 0
hfi' : i ∈ f.support
c : ι
hc : c ∈ f.support.erase i
⊢ c ∈ I
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
a✝ : Additive M
⊢ (AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Additive.ofMul) (x * y).coeff)).coeff a✝ =
    (AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Additive.ofMul) x.coeff) *
          AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Additive.ofMul) y.coeff)).coeff
      a✝

Tactic:
simp [coeff_mul, AddMonoidAlgebra.coeff_mul, sum_mapDomain_index, add_mul, mul_add,
      ite_add_zero, Additive.ext_iff]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
r : R
m : M
inst✝ : Mul M
hm : ∀ (m' : M), Commute m m'
hr : ∀ (r' : R), Commute r r'
x : R[M]
m' : M
r' : R
⊢ ((AddMonoidHom.mulLeft (single m r)).comp (singleAddHom m')) r' =
    ((AddMonoidHom.mulRight (single m r)).comp (singleAddHom m')) r'

Tactic:
exact single_commute_single (hm m') (hr r')

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Monoid M
motive : R[M] → Prop
x : R[M]
of : ∀ (m : M), motive ((MonoidAlgebra.of R M) m)
add : ∀ (x y : R[M]), motive x → motive y → motive (x + y)
smul : ∀ (r : R) (x : R[M]), motive x → motive (r • x)
m : M
r : R
⊢ motive (ofCoeff (Finsupp.single m r))

Tactic:
simpa using smul r (.of R M m) (of m)

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : End R M
p : Submodule R M
hp : p ∈ {p | p ≤ Submodule.comap f p}
q : Submodule R M
hq : q ∈ {p | p ≤ Submodule.comap f p}
⊢ p ⊓ q ∈ {p | p ≤ Submodule.comap f p}

Tactic:
simp only [Set.mem_ofPred_eq, Submodule.comap_inf, le_inf_iff]
    exact ⟨inf_le_of_left_le hp, inf_le_of_right_le hq⟩

Goal state after:
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝³ : Finite ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
⊢ Surjective ⇑((piEquiv ι R M) v) ↔ span R (Set.range v) = ⊤

Tactic:
rw [← LinearMap.range_eq_top, range_piEquiv]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case a.refine_1
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝² : DecidableEq R
this✝¹ : DecidableEq M
this✝ : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
this : Inhabited P
⊢ (lmapDomain R R g) l ∈ supported R R (g '' ↑t1)

Tactic:
← Finsupp.lmapDomain_supported _ _ g,

Goal state after:
case a.refine_1
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝² : DecidableEq R
this✝¹ : DecidableEq M
this✝ : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
this : Inhabited P
⊢ (lmapDomain R R g) l ∈ map (lmapDomain R R g) (supported R R ↑t1)
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h_exact : Function.Exact ⇑f ⇑g
h_surj : Surjective ⇑g
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R P
⊢ (map g ⊤).FG

Tactic:
← LinearMap.range_eq_top

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h_exact : Function.Exact ⇑f ⇑g
h_surj : g.range = ⊤
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R P
⊢ (map g ⊤).FG
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
h₀ : a = 0 → Nonempty ι
⊢ (⨅ i, f i) * a = ⨅ i, f i * a

Tactic:
by
  simp_rw [mul_comm, mul_iInf' h₀]

Goal state after:
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case mpr.mp
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : CommMonoid M₁
inst✝⁴ : CommMonoid M₂
inst✝³ : CommMonoid M₃
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : MulExact ⇑f' ⇑g'
x₂ : M₂
⊢ g x₂ = 1 → x₂ ∈ Set.range ⇑f

Tactic:
intro hx₂
      obtain ⟨y₁, hy₁⟩ := (h (τ₂ x₂)).1 (by simp only [comm₂₃, hx₂, map_one])
      obtain ⟨x₁, rfl⟩ := h₁ y₁
      exact ⟨x₁, h₂.1 (by simpa only [comm₁₂] using hy₁)⟩

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
i : ℕ
hi : i < p.toList.length
⊢ p.toList[i] = p.toFun ⟨i, ⋯⟩

Tactic:
by
  simp only [toList, List.getElem_ofFn]

Goal state after: