mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
g : Ordinal.{u_1} → Ordinal.{u_1}
hg : IsNormal g
hf : IsFundamentalSeq f
ho : IsSuccLimit o
⊢ IsCofinal (range fun i ↦ ⟨g ↑(f i), ⋯⟩)

Tactic:
by
    rintro ⟨b, hb⟩
    rw [mem_Iio, hg.lt_iff_exists_lt ho] at hb
    obtain ⟨c, hc, hc'⟩ := hb
    obtain ⟨_, ⟨d, rfl⟩, hd⟩ := hf.isCofinal_range ⟨c, hc⟩
    refine ⟨⟨_, hg.strictMono (f d).2⟩, ?_, hc'.le.trans (hg.monotone hd)⟩
    simp

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

Goal state before:
pp: case refine_2
o : Ordinal.{u}
S : Set o.ToType
hS : IsCofinal S
hS' : #↑S = Order.cof o.ToType
f : ↑S → Ordinal.{u} := fun s ↦ (typein LT.lt).toRelEmbedding ↑s
a : Ordinal.{u}
ha : a < typeLT o.ToType
b : o.ToType
hb : b ∈ S
hb' : (enum fun x1 x2 ↦ x1 < x2) ⟨a, ha⟩ ≤ b
⊢ a < lsub f

Tactic:
rw [← not_lt, ← typein_le_typein, typein_enum] at hb'

Goal state after:
case refine_2
o : Ordinal.{u}
S : Set o.ToType
hS : IsCofinal S
hS' : #↑S = Order.cof o.ToType
f : ↑S → Ordinal.{u} := fun s ↦ (typein LT.lt).toRelEmbedding ↑s
a : Ordinal.{u}
ha : a < typeLT o.ToType
b : o.ToType
hb : b ∈ S
hb' : a ≤ (typein LT.lt).toRelEmbedding b
⊢ a < lsub f
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

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

Tactic:
rw [Cardinal.lift_umax, c.lift_id']

Goal state after:
case refine_1
ι : 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
⊢ Cardinal.lift.{v, u} #(List ι) < c.cof
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: c : Cardinal.{u}
h : ℵ₀ ≤ c
n : ℕ
hn : 2 ≤ n
⊢ 2 ≤ ↑n

Tactic:
by assumption_mod_cast

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

Goal state before:
pp: case pos
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : i = j
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0

Tactic:
subst hij

Goal state after:
case pos
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i : ι
xi xj : β i
h : single i xi = single i xj
⊢ i = i ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0

Tactic:
have h_coe : ⇑(DFinsupp.single i xi) = DFinsupp.single j xj := congr_arg (⇑) h

Goal state after:
case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ⇑(single i xi) = ⇑(single j xj)
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
Module: Mathlib.Data.List.Pi

Goal state before:
pp: case cons
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
fs : (i : ι) → List (α i)
i : ι
l : List ι
ih : ((↑l).pi fun x ↦ ↑(fs x)) = ↑(l.pi fs)
⊢ ((↑(i :: l)).pi fun x ↦ ↑(fs x)) = ↑((i :: l).pi fs)

Tactic:
simp [ih, Multiset.coe_bind, ← Multiset.cons_coe]

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

Goal state before:
pp: ι : 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)
f : (i : ι) → β i
s : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
⊢ p { toFun := f, support' := s }

Tactic:
induction s using Trunc.induction_on with

Goal state after:
case h
ι : 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)
f : (i : ι) → β i
s : { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
⊢ p { toFun := f, support' := Trunc.mk s }
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: case inr
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x : δ ⟨i, j⟩.fst ⟨i, j⟩.snd
i' : ι
j' : α i'
hi : i ≠ i'
⊢ (single ⟨i, j⟩ x) ⟨i', j'⟩ = ((single i (single j x)) i') j'

Tactic:
simp [hi]

Goal state after:
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: case refine_1
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
e : Quotient (Subtype.instSetoid_mathlib fun l ↦ ∀ (i : ι), i ∈ l) :=
  (Equiv.subtypeQuotientEquivQuotientSubtype (fun l ↦ ∀ (i : ι), i ∈ l) (fun s ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯)
    ⟨Finset.univ.val, ⋯⟩
l : { l // ∀ (i : ι), i ∈ l }
⊢ ∀ ⦃a b : (i : ι) → i ∈ ↑l → α i⦄, a ≈ b → (fun i ↦ a i ⋯) ≈ fun i ↦ b i ⋯

pp: case refine_2
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
e : Quotient (Subtype.instSetoid_mathlib fun l ↦ ∀ (i : ι), i ∈ l) :=
  (Equiv.subtypeQuotientEquivQuotientSubtype (fun l ↦ ∀ (i : ι), i ∈ l) (fun s ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯)
    ⟨Finset.univ.val, ⋯⟩
⊢ ∀ (a b : { l // ∀ (i : ι), i ∈ l }),
    a ≈ b →
      Quotient.map (fun a_2 i ↦ a_2 i ⋯) ⋯ (listChoice fun i x ↦ q i) =
        Quotient.map (fun a i ↦ a i ⋯) ⋯ (listChoice fun i x ↦ q i)

Tactic:
· exact fun _ _ h i ↦ h i _

Goal state after:
case refine_2
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
e : Quotient (Subtype.instSetoid_mathlib fun l ↦ ∀ (i : ι), i ∈ l) :=
  (Equiv.subtypeQuotientEquivQuotientSubtype (fun l ↦ ∀ (i : ι), i ∈ l) (fun s ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯)
    ⟨Finset.univ.val, ⋯⟩
⊢ ∀ (a b : { l // ∀ (i : ι), i ∈ l }),
    a ≈ b →
      Quotient.map (fun a_2 i ↦ a_2 i ⋯) ⋯ (listChoice fun i x ↦ q i) =
        Quotient.map (fun a i ↦ a i ⋯) ⋯ (listChoice fun i x ↦ q i)
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : (i : ι) → β i
s : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
⊢ i ∈ { toFun := f, support' := s }.support ↔ { toFun := f, support' := s } i ≠ 0

Tactic:
induction s using Trunc.induction_on with

Goal state after:
case h
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : (i : ι) → β i
s : { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
⊢ i ∈ { toFun := f, support' := Trunc.mk s }.support ↔ { toFun := f, support' := Trunc.mk s } i ≠ 0
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: case inr
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → (j : α i) → Zero (δ i j)
inst✝ : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
i' : ι
j' : α i'
hi : i ≠ i'
⊢ ((single i (single j x)) i') j' = (single ⟨i, j⟩ x) ⟨i', j'⟩

Tactic:
simp [hi]

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

Goal state before:
pp: R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
⊢ Surjective (Sum.elim (fun i ↦ ⟨(inl R M M') ↑i, ⋯⟩) fun i ↦ ⟨(inr R M M') ↑i, ⋯⟩)

Tactic:
rintro ⟨_, ⟨_, _, rfl⟩ | ⟨_, _, rfl⟩⟩

Goal state after:
case inl
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
w✝ : M
left✝ : w✝ ∈ s
⊢ ∃ a, Sum.elim (fun i ↦ ⟨(inl R M M') ↑i, ⋯⟩) (fun i ↦ ⟨(inr R M M') ↑i, ⋯⟩) a = ⟨(inl R M M') w✝, ⋯⟩

case inr
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
w✝ : M'
left✝ : w✝ ∈ t
⊢ ∃ a, Sum.elim (fun i ↦ ⟨(inl R M M') ↑i, ⋯⟩) (fun i ↦ ⟨(inr R M M') ↑i, ⋯⟩) a = ⟨(inr R M M') w✝, ⋯⟩
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
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • u • x + t • u • y = 0
⊢ (u • s) • x + (u • t) • y = 0

Tactic:
by rw [smul_assoc, smul_assoc, smul_comm u s, smul_comm u t, hst]

Goal state after:
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
x✝ : X
⊢ 1 • of x✝ = (AddMonoidHom.id (FreeAbelianGroup X)) (of x✝)

Tactic:
one_smul,

Goal state after:
X : Type u_1
x✝ : X
⊢ of x✝ = (AddMonoidHom.id (FreeAbelianGroup X)) (of x✝)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case hf
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd : ∀ (i : η) (t : Set η), t.Finite → i ∉ t → Disjoint (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
⊢ Injective fun ji ↦ f ji.fst ji.snd

Tactic:
rintro ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ hxy
    by_cases h_cases : x₁ = y₁
    · subst h_cases
      refine Sigma.eq rfl ?_
      rw [LinearIndependent.injective (hindep _) hxy]
    · have h0 : f x₁ x₂ = 0 := by
        apply
          disjoint_def.1 (hd x₁ {y₁} (finite_singleton y₁) fun h => h_cases (eq_of_mem_singleton h))
            (f x₁ x₂) (subset_span (mem_range_self _))
        rw [iSup_singleton]
        simp only at hxy
        rw [hxy]
        exact subset_span (mem_range_self y₂)
      exact False.elim ((hindep x₁).ne_zero _ h0)

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : DecidableEq ι
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
hf : ∀ (l : ι →₀ R), (linearCombination R f) l = 0 → l = 0
i : ι
m : M
r : R
hr : r ∈ nonZeroDivisors R
l : ι →₀ R
hl : l i ∈ nonZeroDivisors R
hg : r • m = (linearCombination R f) l
l' : ι →₀ R
hl' : (linearCombination R f) (r • l') - r • l' i • f i + (linearCombination R f) (l' i • l) = 0
⊢ l' = 0

Tactic:
smul_smul,

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : DecidableEq ι
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
hf : ∀ (l : ι →₀ R), (linearCombination R f) l = 0 → l = 0
i : ι
m : M
r : R
hr : r ∈ nonZeroDivisors R
l : ι →₀ R
hl : l i ∈ nonZeroDivisors R
hg : r • m = (linearCombination R f) l
l' : ι →₀ R
hl' : (linearCombination R f) (r • l') - (r * l' i) • f i + (linearCombination R f) (l' i • l) = 0
⊢ l' = 0
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: case ofNat
A : Type u_1
M : Type u_2
inst✝¹ : AddCommGroup A
inst✝ : DivisionCommMonoid M
ψ : AddChar A M
a : A
a✝ : ℕ
⊢ (Int.ofNat a✝ • ψ) a = ψ a ^ Int.ofNat a✝

Tactic:
simp [-neg_apply, neg_apply']

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

Goal state before:
pp: case negSucc
A : Type u_1
M : Type u_2
inst✝¹ : AddCommGroup A
inst✝ : DivisionCommMonoid M
ψ : AddChar A M
a : A
a✝ : ℕ
⊢ (Int.negSucc a✝ • ψ) a = ψ a ^ Int.negSucc a✝

Tactic:
simp [-neg_apply, neg_apply']

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)
⊢ g '' image2 f ↑s ↑t = image2 f' (↑s) (g' '' ↑t)

Tactic:
exact image_image2_distrib_right h_distrib

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

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
δ : Type u_7
ε : Type u_9
inst✝³ : DecidableEq α'
inst✝² : DecidableEq β'
inst✝¹ : DecidableEq ε
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
γ : Type u_14
u : Finset γ
f : δ → γ → ε
g : α → β → δ
f₁ : α → γ → α'
f₂ : β → γ → β'
g' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f₁ a c) (f₂ b c)
⊢ image2 f (image2 g ↑s ↑t) ↑u ⊆ image2 g' (image2 f₁ ↑s ↑u) (image2 f₂ ↑t ↑u)

Tactic:
exact Set.image2_distrib_subset_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
eq : {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} = t
⊢ ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = t.card

Tactic:
apply
    Exists.elim
      (this (t.filter fun x => x ∉ s) (t.filter fun x => x ∈ s) (by simp [Set.subset_def])
        (by simp +contextual [Set.ext_iff]) (by rwa [eq]))

Goal state after:
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
eq : {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} = t
⊢ ∀ (a : Finset V),
    ↑a ⊆ s ∪ ↑({x ∈ t | x ∉ s}) ∧ s ⊆ ↑a ∧ a.card = ({x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s}).card →
      ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = t.card
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
eq : {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} = t
⊢ ∀ (a : Finset V),
    ↑a ⊆ s ∪ ↑({x ∈ t | x ∉ s}) ∧ s ⊆ ↑a ∧ a.card = ({x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s}).card →
      ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = t.card

Tactic:
intro u

Goal state after:
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
eq : {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} = t
u : Finset V
⊢ ↑u ⊆ s ∪ ↑({x ∈ t | x ∉ s}) ∧ s ⊆ ↑u ∧ u.card = ({x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s}).card →
    ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = t.card
Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors

Goal state before:
pp: case H.inr
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : IsCancelAdd R
inst✝² : IsLeftCancelMulZero R
inst✝¹ : Mul A
inst✝ : UniqueProds A
f g₁ g₂ : R[A]
ih :
  ∀ s ∈ g₁.coeff.support ∪ g₂.coeff.support,
    ∀ {g₁_1 g₂_1 : R[A]},
      (fun x ↦ f * x) g₁_1 = (fun x ↦ f * x) g₂_1 →
        g₁_1.coeff.support ∪ g₂_1.coeff.support = (g₁.coeff.support ∪ g₂.coeff.support).erase s → g₁_1 = g₂_1
h✝ : (g₁.coeff.support ∪ g₂.coeff.support).Nonempty
hf : f.coeff.support.Nonempty
af : A
haf : af ∈ f.coeff.support
ag : A
hag : ag ∈ g₁.coeff.support ∪ g₂.coeff.support
uniq : UniqueMul f.coeff.support (g₁.coeff.support ∪ g₂.coeff.support) af ag
h : f.coeff af * g₂.coeff ag = f.coeff af * g₁.coeff ag
this : g₂.coeff ag = g₁.coeff ag
eq : f * erase ag g₁ = f * erase ag g₂
⊢ erase ag g₁ + single ag (g₁.coeff ag) = erase ag g₂ + single ag (g₁.coeff ag)

Tactic:
ih ag hag eq

Goal state after:
case H.inr
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : IsCancelAdd R
inst✝² : IsLeftCancelMulZero R
inst✝¹ : Mul A
inst✝ : UniqueProds A
f g₁ g₂ : R[A]
ih :
  ∀ s ∈ g₁.coeff.support ∪ g₂.coeff.support,
    ∀ {g₁_1 g₂_1 : R[A]},
      (fun x ↦ f * x) g₁_1 = (fun x ↦ f * x) g₂_1 →
        g₁_1.coeff.support ∪ g₂_1.coeff.support = (g₁.coeff.support ∪ g₂.coeff.support).erase s → g₁_1 = g₂_1
h✝ : (g₁.coeff.support ∪ g₂.coeff.support).Nonempty
hf : f.coeff.support.Nonempty
af : A
haf : af ∈ f.coeff.support
ag : A
hag : ag ∈ g₁.coeff.support ∪ g₂.coeff.support
uniq : UniqueMul f.coeff.support (g₁.coeff.support ∪ g₂.coeff.support) af ag
h : f.coeff af * g₂.coeff ag = f.coeff af * g₁.coeff ag
this : g₂.coeff ag = g₁.coeff ag
eq : f * erase ag g₁ = f * erase ag g₂
⊢ erase ag g₂ + single ag (g₁.coeff ag) = erase ag g₂ + single ag (g₁.coeff ag)

case H.inr
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : IsCancelAdd R
inst✝² : IsLeftCancelMulZero R
inst✝¹ : Mul A
inst✝ : UniqueProds A
f g₁ g₂ : R[A]
ih :
  ∀ s ∈ g₁.coeff.support ∪ g₂.coeff.support,
    ∀ {g₁_1 g₂_1 : R[A]},
      (fun x ↦ f * x) g₁_1 = (fun x ↦ f * x) g₂_1 →
        g₁_1.coeff.support ∪ g₂_1.coeff.support = (g₁.coeff.support ∪ g₂.coeff.support).erase s → g₁_1 = g₂_1
h✝ : (g₁.coeff.support ∪ g₂.coeff.support).Nonempty
hf : f.coeff.support.Nonempty
af : A
haf : af ∈ f.coeff.support
ag : A
hag : ag ∈ g₁.coeff.support ∪ g₂.coeff.support
uniq : UniqueMul f.coeff.support (g₁.coeff.support ∪ g₂.coeff.support) af ag
h : f.coeff af * g₂.coeff ag = f.coeff af * g₁.coeff ag
this : g₂.coeff ag = g₁.coeff ag
eq : f * erase ag g₁ = f * erase ag g₂
⊢ (erase ag g₁).coeff.support ∪ (erase ag g₂).coeff.support = (g₁.coeff.support ∪ g₂.coeff.support).erase ag
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Mul G
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq G
ha0 : a0 ∈ A
hb0 : b0 ∈ B
h : UniqueMul A B a0 b0
p1 p2 : G × G
x✝¹ : (p1.1 ∈ A ∧ p1.2 ∈ B) ∧ p1.1 * p1.2 = a0 * b0
x✝ : (p2.1 ∈ A ∧ p2.2 ∈ B) ∧ p2.1 * p2.2 = a0 * b0
ha1 : p1.1 ∈ A
hb1 : p1.2 ∈ B
he1 : p1.1 * p1.2 = a0 * b0
ha2 : p2.1 ∈ A
hb2 : p2.2 ∈ B
he2 : p2.1 * p2.2 = a0 * b0
h1 : p1.1 = a0 ∧ p1.2 = b0
⊢ p1 = p2

Tactic:
have h2 := h ha2 hb2 he2

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Mul G
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq G
ha0 : a0 ∈ A
hb0 : b0 ∈ B
h : UniqueMul A B a0 b0
p1 p2 : G × G
x✝¹ : (p1.1 ∈ A ∧ p1.2 ∈ B) ∧ p1.1 * p1.2 = a0 * b0
x✝ : (p2.1 ∈ A ∧ p2.2 ∈ B) ∧ p2.1 * p2.2 = a0 * b0
ha1 : p1.1 ∈ A
hb1 : p1.2 ∈ B
he1 : p1.1 * p1.2 = a0 * b0
ha2 : p2.1 ∈ A
hb2 : p2.2 ∈ B
he2 : p2.1 * p2.2 = a0 * b0
h1 : p1.1 = a0 ∧ p1.2 = b0
h2 : p2.1 = a0 ∧ p2.2 = b0
⊢ p1 = p2
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : 0 < (s.sort fun a b ↦ a ≤ b).length
H : s.Nonempty
⊢ (s.sort fun a b ↦ a ≤ b).get ⟨0, h⟩ = s.min' H

Tactic:
let l := s.sort

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : 0 < (s.sort fun a b ↦ a ≤ b).length
H : s.Nonempty
l : List α := s.sort fun a b ↦ a ≤ b
⊢ (s.sort fun a b ↦ a ≤ b).get ⟨0, h⟩ = s.min' H
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ ↑(s ^ n) = ↑s ^ n

Tactic:
by
  change ↑(npowRec n s) = (s : Set α) ^ n
  induction n with
  | zero => rw [npowRec, pow_zero, coe_one]
  | succ n ih => rw [npowRec, pow_succ, coe_mul, ih]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : (s.sort fun a b ↦ a ≤ b).length - 1 < (s.sort fun a b ↦ a ≤ b).length
H : s.Nonempty
⊢ (s.sort fun a b ↦ a ≤ b)[(s.sort fun a b ↦ a ≤ b).length - 1] = s.max' H

Tactic:
let l := s.sort

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : (s.sort fun a b ↦ a ≤ b).length - 1 < (s.sort fun a b ↦ a ≤ b).length
H : s.Nonempty
l : List α := s.sort fun a b ↦ a ≤ b
⊢ (s.sort fun a b ↦ a ≤ b)[(s.sort fun a b ↦ a ≤ b).length - 1] = s.max' H
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : (s.sort fun a b ↦ a ≤ b).length - 1 < (s.sort fun a b ↦ a ≤ b).length
⊢ s.Nonempty

Tactic:
rw [length_sort] at h; exact card_pos.1 (lt_of_le_of_lt bot_le h)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : (s.sort fun a b ↦ a ≤ b).length - 1 < (s.sort fun a b ↦ a ≤ b).length
⊢ s.Nonempty

Tactic:
by rw [length_sort] at h; exact card_pos.1 (lt_of_le_of_lt bot_le h)

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Semigroup G
inst✝ : IsCancelMul G
h : ∀ {A : Finset G}, A.Nonempty → ∃ a1 ∈ A, ∃ a2 ∈ A, UniqueMul A A a1 a2
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
by
    classical
    obtain ⟨g1, h1, g2, h2, hu⟩ := h (hB.mul hA)
    obtain ⟨b1, hb1, a1, ha1, rfl⟩ := mem_mul.mp h1
    obtain ⟨b2, hb2, a2, ha2, rfl⟩ := mem_mul.mp h2
    refine ⟨a1, ha1, b2, hb2, fun a b ha hb he => ?_⟩
    specialize hu (mul_mem_mul hb1 ha) (mul_mem_mul hb ha2) _
    · rw [mul_assoc b1, ← mul_assoc a, he, mul_assoc a1, ← mul_assoc b1]
    exact ⟨mul_left_cancel hu.1, mul_right_cancel hu.2⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
p : ι → Submodule R M
m : M
hm : m ∈ ⨆ i, p i
⊢ ∃ s, m ∈ ⨆ i ∈ s, p i

Tactic:
by
  have :=
    CompleteLattice.IsCompactElement.exists_finset_of_le_iSup (Submodule R M)
      (Submodule.singleton_span_isCompactElement m) p
  simp only [Submodule.span_singleton_le_iff_mem] at this
  exact this hm

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

Goal state before:
pp: case refine_3
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu✝ : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x✝ : Mul (Finset G) := Finset.mul
e f : G
he : ∃ y, (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = e
hf : ∃ y ∈ D, ∃ z, (∃ a ∈ C, a⁻¹ = z) ∧ y * z = f
hu :
  ∀ ⦃a b : G⦄,
    (∃ y, (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
      (∃ y ∈ D, ∃ z, (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) → a * b = e * f → a = e ∧ b = f
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d

Tactic:
obtain ⟨_, ⟨d1, hd1, rfl⟩, c1, hc1, rfl⟩ := he

Goal state after:
case refine_3
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu✝ : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x✝ : Mul (Finset G) := Finset.mul
f : G
hf : ∃ y ∈ D, ∃ z, (∃ a ∈ C, a⁻¹ = z) ∧ y * z = f
d1 : G
hd1 : d1 ∈ D
c1 : G
hc1 : c1 ∈ C
hu :
  ∀ ⦃a b : G⦄,
    (∃ y, (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
      (∃ y ∈ D, ∃ z, (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) → a * b = d1⁻¹ * c1 * f → a = d1⁻¹ * c1 ∧ b = f
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
hpq : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
⊢ ofIsCompl hpq φ ψ = φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯

Tactic:
by
  ext x
  obtain ⟨a, b, rfl, _⟩ := existsUnique_add_of_isCompl hpq x
  simp

Goal state after: