mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case e'_2
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ a = ⨆ i, ↑i

pp: case convert_2
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ Nonempty ↑(Iio a)

pp: case convert_4
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ BddAbove (range Subtype.val)

Tactic:
· exact ha.iSup_Iio.symm

Goal state after:
case convert_2
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ Nonempty ↑(Iio a)

case convert_4
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ BddAbove (range Subtype.val)
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
inst✝⁴ : LinearOrder α
inst✝³ : WellFoundedLT α
inst✝² : SuccOrder α
inst✝¹ : LinearOrder β
inst✝ : OrderBot α
g : α → β
hf : IsNormal f
hg : IsNormal g
⊢ (f ⊥ = g ⊥ ∧ ∀ (a : α), f a = g a → f (succ a) = g (succ a)) → f = g

Tactic:
rintro ⟨H₁, H₂⟩

Goal state after:
case mpr
α : Type u_1
β : Type u_2
f : α → β
inst✝⁴ : LinearOrder α
inst✝³ : WellFoundedLT α
inst✝² : SuccOrder α
inst✝¹ : LinearOrder β
inst✝ : OrderBot α
g : α → β
hf : IsNormal f
hg : IsNormal g
H₁ : f ⊥ = g ⊥
H₂ : ∀ (a : α), f a = g a → f (succ a) = g (succ a)
⊢ f = g
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 : α
⊢ ∃ b, f (Sum.inr a) = Sum.inr b

Tactic:
generalize hx : f (Sum.inr a) = x

Goal state after:
α✝ : 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
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
⊢ cof α = #α

Tactic:
by
  rw [← card_type LT.lt, ← ord_cof_eq_type_lt, card_ord]

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

Goal state before:
pp: a b c : Ordinal.{u_4}
hc : IsSuccLimit c
⊢ a < b + c ↔ ∃ d < c, a < b + d

Tactic:
rw [lt_add_iff hc.ne_bot]
  constructor <;> rintro ⟨d, hd, ha⟩
  · refine ⟨_, hc.succ_lt hd, ?_⟩
    rwa [succ_eq_add_one, ← add_assoc, lt_add_one_iff]
  · exact ⟨d, hd, ha.le⟩

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

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
g : Ordinal.{v} → Ordinal.{max v w}
⊢ BddAbove (range (g ∘ f))

Tactic:
by
  rw [range_comp]
  exact bddAbove_image hf g

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

Goal state before:
pp: case mp.refine_2
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = typeLT α
b : α
⊢ b ≤ (enum fun x1 x2 ↦ x1 < x2) ⟨a, ⋯⟩

Tactic:
← enum_typein (α := α) (· < ·) b,

Goal state after:
case mp.refine_2
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = typeLT α
b : α
⊢ (enum fun x1 x2 ↦ x1 < x2) ⟨(typein fun x1 x2 ↦ x1 < x2).toRelEmbedding b, ⋯⟩ ≤ (enum fun x1 x2 ↦ x1 < x2) ⟨a, ⋯⟩
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max v u_3}
⊢ lsub f = 0 ↔ IsEmpty ι

Tactic:
refine ⟨fun h => ⟨fun i => ?_⟩, fun h => @lsub_empty _ h _⟩

Goal state after:
ι : Type u_3
f : ι → Ordinal.{max v u_3}
h : lsub f = 0
i : ι
⊢ False
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
ho : IsSuccPrelimit o
⊢ sSup (range ⇑(typein fun x1 x2 ↦ x1 < x2).toRelEmbedding) = o

Tactic:
PrincipalSeg.range_eq

Goal state after:
o : Ordinal.{u}
ho : IsSuccPrelimit o
⊢ sSup {b | b < (typein fun x1 x2 ↦ x1 < x2).top} = o
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u_3}
⊢ sSup (range ⇑(typein fun x1 x2 ↦ x1 < x2).toRelEmbedding) = sSup (Iic o)

Tactic:
PrincipalSeg.range_eq

Goal state after:
o : Ordinal.{u_3}
⊢ sSup {b | b < (typein fun x1 x2 ↦ x1 < x2).top} = sSup (Iic o)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl.inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a = 0
⊢ a ^ 1 ≤ a ^ b

Tactic:
rw [a0, zero_opow one_ne_zero]

Goal state after:
case inl.inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a = 0
⊢ 0 ≤ 0 ^ b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ IsSuccLimit c.ord

Tactic:
constructor
  · simpa using (aleph0_pos.trans_le hc).ne'
  · simp_rw [isSuccPrelimit_iff_succ_lt, succ_eq_add_one, lt_ord, card_add_one]
    refine fun a ha ↦ ?_
    contrapose! ha
    rwa [add_one_of_aleph0_le] at ha
    rw [← ord_le, ← IsSuccLimit.le_succ_iff, succ_eq_add_one, ord_le, card_add_one]
    · exact hc.trans ha
    · simp

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

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
i : ι
⊢ nfpFamily f (succ a) ∈ (fun i ↦ fixedPoints (f i)) i

Tactic:
exact nfpFamily_fp (H i) _

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

Goal state before:
pp: case succ
o : Ordinal.{u_1}
a✝ : ¬IsMax o
IH : lift.{v, u_1} (preBeth o) = preBeth (Ordinal.lift.{v, u_1} o)
⊢ lift.{v, u_1} (preBeth (succ o)) = preBeth (Ordinal.lift.{v, u_1} (succ o))

Tactic:
| succ o _ IH =>

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

Goal state before:
pp: o : Ordinal.{u}
n : ℕ
⊢ ω_ ↑n < lift.{v, u} o ↔ ω_ ↑n < o

Tactic:
simpa using lift_lt (a := ω_ n)

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

Goal state before:
pp: case refine_2.hg
a o o' : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}
hg : o.IsFundamentalSequence o' g
⊢ o'.blsub g = o

Tactic:
· exact hg.2.2

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

Goal state before:
pp: case add_one.h'
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ ¬(a = 0 ∧ b ≠ 0)

Tactic:
rintro ⟨rfl, -⟩

Goal state after:
case add_one.h'
b : Ordinal.{u_1}
ha : ω ≤ 0
IH : (0 ^ b).card ≤ max (card 0) b.card
⊢ False
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι
b : Cardinal.{u}
x✝ : b ∈ {a | ∃ ι f, lsub f = o ∧ #ι = a}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
hb : #ι = b
⊢ a ≤ b

Tactic:
← hb

Goal state after:
o : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι
b : Cardinal.{u}
x✝ : b ∈ {a | ∃ ι f, lsub f = o ∧ #ι = a}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
hb : #ι = b
⊢ a ≤ #ι
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι
b : Cardinal.{u}
x✝ : b ∈ {a | ∃ ι f, lsub f = o ∧ #ι = a}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
hb : #ι = b
⊢ a ≤ b

Tactic:
rw [← hb]
        exact H _ hf

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

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

Tactic:
rwa [Cardinal.lift_umax, lift_id']

Goal state after:
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
⊢ Cardinal.lift.{max u v, u} #ι < (lift.{u, max u v} c).cof

Tactic:
rwa [Cardinal.lift_umax, lift_id']

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:
by
  apply (card_opow_le_of_omega0_le_right a hb).antisymm (max_le _ _) <;> apply card_le_card
  · exact left_le_opow a (omega0_pos.trans_le hb)
  · exact right_le_opow b ha

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

Goal state before:
pp: case refine_2.cons
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{max u v}
ha : a < c
i : ι
l : List ι
H : List.foldr f a l < c
⊢ List.foldr f a (i :: l) < c

Tactic:
| cons i l H =>

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (ℵ_ o).IsSingular ↔ IsSuccLimit o ∧ o.cof < ℵ_ o

Tactic:
obtain rfl | ⟨a, rfl⟩ | ho := zero_or_succ_or_isSuccLimit o
  · simp
  · simp
  · rw [isSingular_iff, ← (cof_ord_le _).lt_iff_ne]
    simp [ho]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: case some
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
r : range v ⊆ range v'
r' : b i ∉ range v
r'' : range v ≠ range v'
l l' : Option κ →₀ R
z : l none • b i + (linearCombination R v) l.some = l' none • b i + (linearCombination R v) l'.some
a : κ
l₁ : l.some = l'.some
⊢ l (Option.some a) = l' (Option.some a)

Tactic:
exact DFunLike.congr_fun l₁ a

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case h.cons
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)
i : ι
s : Multiset ι
ih : ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0), p { toFun := f, support' := Trunc.mk ⟨s, H⟩ }
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 : p (erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })
H3 :
  single i ({ toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } i) +
      erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } =
    { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ }
⊢ p (single i (f i) + erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })

Tactic:
rcases Classical.em (f i = 0) with h | h

Goal state after:
case h.cons.inl
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)
i : ι
s : Multiset ι
ih : ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0), p { toFun := f, support' := Trunc.mk ⟨s, H⟩ }
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 : p (erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })
H3 :
  single i ({ toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } i) +
      erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } =
    { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ }
h : f i = 0
⊢ p (single i (f i) + erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })

case h.cons.inr
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)
i : ι
s : Multiset ι
ih : ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0), p { toFun := f, support' := Trunc.mk ⟨s, H⟩ }
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 : p (erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })
H3 :
  single i ({ toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } i) +
      erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } =
    { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ }
h : ¬f i = 0
⊢ p (single i (f i) + erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst✝ : (i : Option ι) → Zero (α i)
f : Π₀ (i : Option ι), α i
⊢ (fun f ↦ extendWith f.1 f.2) ((fun f ↦ (f none, comapDomain some ⋯ f)) f) = f

Tactic:
ext i; obtain - | i := i
    · rw [extendWith_none]
    · rw [extendWith_some, comapDomain_apply]

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → β₁ i ≃+ β₂ i
x : Π₀ (i : ι), β₁ i
⊢ mapRange (fun i ↦ (fun x ↦ (e i).symm x) ∘ fun x ↦ (e i) x) ?h x = x

Tactic:
simp_rw [AddEquiv.symm_comp_self]
          simp

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → β₁ i ≃+ β₂ i
x : Π₀ (i : ι), β₁ i
⊢ ∀ (i : ι), ((fun x ↦ (e i).symm x) ∘ fun x ↦ (e i) x) 0 = 0

Tactic:
simp_rw [AddEquiv.symm_comp_self]
          simp

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : LinearIndependent R ![x, y]
s t : R
h' : s • x = t • y
⊢ s = 0 ∧ 0 = t

Tactic:
exact h.eq_of_pair (by simpa using h')

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ LinearIndependent R ![-y, x] ↔ LinearIndependent R ![x, y]

Tactic:
pair_neg_left_iff,

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ LinearIndependent R ![y, x] ↔ LinearIndependent R ![x, y]
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval - l₂.eval = l.eval
⊢ ((r₁, x) ::ᵣ l₁).eval - ((r₂, x) ::ᵣ l₂).eval = ((r₁ - r₂, x) ::ᵣ l).eval

Tactic:
simp only [← h, eval_cons, sub_eq_add_neg, neg_add, add_smul, neg_smul, add_assoc]
  congr! 1
  simp only [← add_assoc]
  congr! 1
  rw [add_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
h' : a • s + c • t = 0 ∧ b • s + d • t = 0
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
⊢ s = 0 ∧ t = 0

Tactic:
obtain ⟨h₁, h₂⟩ := h'

Goal state after:
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ s = 0 ∧ t = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_6
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : span R (Set.range v) = ⊤
hli : LinearIndependent R (⇑f ∘ v)
⊢ Injective ⇑f

Tactic:
by
  refine (injective_iff_map_eq_zero _).mpr fun x hx ↦ ?_
  have : x ∈ Submodule.span R (.range v) := by rw [hv]; exact mem_top
  obtain ⟨c, rfl⟩ := Finsupp.mem_span_range_iff_exists_finsupp.mp this
  simp only [map_finsuppSum, map_smul] at hx
  obtain rfl := linearIndependent_iff.mp hli c hx
  simp

Goal state after:
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
n : ℕ
⊢ ψ ^ n = ψ.mulShift ↑n

Tactic:
by
  ext x
  rw [pow_apply, ← mulShift_spec']

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
a : V
h : LinearIndepOn K id s
⊢ a ∈ span K s ↔ LinearIndepOn K id (insert a s) → a ∈ s

Tactic:
by
  simpa using h.mem_span_iff (a := a)

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
l : List (Set α)
a : α
⊢ a ∈ l.prod ↔ ∃ l', (List.map (fun x ↦ ↑x.snd) l').prod = a ∧ List.map Sigma.fst l' = l

Tactic:
induction l using List.ofFnRec with

Goal state after:
case h
α : Type u_1
inst✝ : Monoid α
a : α
n : ℕ
f : Fin n → Set α
⊢ a ∈ (List.ofFn f).prod ↔ ∃ l', (List.map (fun x ↦ ↑x.snd) l').prod = a ∧ List.map Sigma.fst l' = List.ofFn f
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
a : α
inst✝ : DecidableEq α
⊢ image2 f (insert a ↑s) ↑t = (fun b ↦ f a b) '' ↑t ∪ image2 f ↑s ↑t

Tactic:
exact image2_insert_left

Goal state after:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq β'
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
g : γ → δ
f' : α → β' → δ
g' : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)
⊢ ↑(image g (image₂ f s t)) = ↑(image₂ f' s (image g' t))

Tactic:
by
    push_cast
    exact image_image2_distrib_right h_distrib

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
t : Finset V
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K ↑t)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
x : V
⊢ x ∈ {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} ↔ x ∈ t

Tactic:
by_cases x ∈ s <;> simp [*]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
m m' : M
inst✝ : Mul M
r : R
x : R[M]
h : ∀ (d : M), d * m ≠ m'
⊢ (x * single m r).coeff m' = 0

Tactic:
classical simp [coeff_mul, h]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
m m' : M
inst✝ : Mul M
r : R
x : R[M]
h : ∀ (d : M), m * d ≠ m'
⊢ (single m r * x).coeff m' = 0

Tactic:
classical simp [coeff_mul, h]

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Mul G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
hA1 : ∀ {a b : G}, a ∈ A → b ∈ A → a = b
hB1 : ∀ {a b : G}, a ∈ B → b ∈ B → a = b
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

Tactic:
obtain ⟨a, ha⟩ := hA

Goal state after:
G : Type u_1
inst✝ : Mul G
A B : Finset G
hB : B.Nonempty
hA1 : ∀ {a b : G}, a ∈ A → b ∈ A → a = b
hB1 : ∀ {a b : G}, a ∈ B → b ∈ B → a = b
a : G
ha : a ∈ A
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
s : Finset α
r : α → α → Prop
inst✝⁴ : DecidableRel r
inst✝³ : IsTrans α r
inst✝² : Std.Antisymm r
inst✝¹ : Std.Total r
inst✝ : DecidableEq α
a : α
h₁ : ∀ b ∈ s, r a b
h₂ : a ∉ s
⊢ (cons a s h₂).sort r = a :: s.sort r

Tactic:
sort_cons r h₁

Goal state after:
α : Type u_1
s : Finset α
r : α → α → Prop
inst✝⁴ : DecidableRel r
inst✝³ : IsTrans α r
inst✝² : Std.Antisymm r
inst✝¹ : Std.Total r
inst✝ : DecidableEq α
a : α
h₁ : ∀ b ∈ s, r a b
h₂ : a ∉ s
⊢ a :: s.sort r = a :: s.sort r
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
⊢ Set.range ⇑(s.orderEmbOfFin h) = ↑s

Tactic:
simp only [orderEmbOfFin, Set.range_comp ((↑) : _ → α) (s.orderIsoOfFin h),
  RelEmbedding.coe_trans, Set.image_univ, Finset.orderEmbOfFin, RelIso.range_eq,
    OrderEmbedding.coe_subtype, OrderIso.coe_toOrderEmbedding,
    Subtype.range_coe_subtype, Finset.setOfPred_mem]

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : UniqueProds G
A B : Finset H
A0 : A.Nonempty
B0 : B.Nonempty
a0 : G
ha0 : a0 ∈ image (⇑f) A
b0 : G
hb0 : b0 ∈ image (⇑f) B
h : UniqueMul (image (⇑f) A) (image (⇑f) B) a0 b0
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
obtain ⟨a', ha', rfl⟩ := mem_image.mp ha0

Goal state after:
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : UniqueProds G
A B : Finset H
A0 : A.Nonempty
B0 : B.Nonempty
b0 : G
hb0 : b0 ∈ image (⇑f) B
a' : H
ha' : a' ∈ A
ha0 : f a' ∈ image (⇑f) A
h : UniqueMul (image (⇑f) A) (image (⇑f) B) (f a') b0
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
u : (Finset α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ {b} * ↑u = {1}

Tactic:
← hb

Goal state after:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
u : (Finset α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ ↑u⁻¹ * ↑u = {1}
Module: Mathlib.LinearAlgebra.FreeModule.Basic

Goal state before:
pp: R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Semiring R'
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R' M'
σ : R →+* R'
σ' : R' →+* R
inst✝² : RingHomInvPair σ σ'
inst✝¹ : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] M'
inst✝ : Free R M
e₁ : R ≃+* R' := RingHomInvPair.toRingEquiv σ σ'
I : Type u_4 := ChooseBasisIndex R M
⊢ Free R' M'

Tactic:
obtain ⟨e₃ : M ≃ₗ[R] I →₀ R⟩ := Module.Free.chooseBasis R M

Goal state after:
R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Semiring R'
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R' M'
σ : R →+* R'
σ' : R' →+* R
inst✝² : RingHomInvPair σ σ'
inst✝¹ : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] M'
inst✝ : Free R M
e₁ : R ≃+* R' := RingHomInvPair.toRingEquiv σ σ'
I : Type u_4 := ChooseBasisIndex R M
e₃ : M ≃ₗ[R] I →₀ R
⊢ Free R' M'
Module: Mathlib.LinearAlgebra.FreeModule.Basic

Goal state before:
pp: case pos
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
f : End R M
h : ∀ (g : End R M) (x : M), g (f x) = f (g x)
h✝ : Subsingleton M
⊢ ∃ α, ∃ (h : ∀ (g : R), g * α = α * g), ∀ (x : M), f x = (smulLeft α ⋯) x

Tactic:
exact ⟨0, by simp, fun _ ↦ Subsingleton.allEq _ _⟩

Goal state after: