mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: 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 }

Tactic:
| _ s
   => 

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 inl.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
j' : α i
hj : j' ≠ j
⊢ (single ⟨i, j⟩ x) ⟨i, j'⟩ = (single j x) j'

Tactic:
rw [single_eq_of_ne, single_eq_of_ne hj]
      simpa using hj

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

Goal state before:
pp: 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

Tactic:
| _ s
   => 

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.BigOperators

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝⁵ : DecidableEq ι
ι₁ : Type u₁
inst✝⁴ : DecidableEq ι₁
β₁ : ι₁ → Type v₁
inst✝³ : (i₁ : ι₁) → Zero (β₁ i₁)
inst✝² : (i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i₁ : ι₁), β₁ i₁
g : (i₁ : ι₁) → β₁ i₁ → Π₀ (i : ι), β i
⊢ (f.sum g).support ⊆ f.support.biUnion fun i ↦ (g i (f i)).support

Tactic:
by
  have :
    ∀ i₁ : ι,
      (f.sum fun (i : ι₁) (b : β₁ i) => (g i b) i₁) ≠ 0 → ∃ i : ι₁, f i ≠ 0 ∧ ¬(g i (f i)) i₁ = 0 :=
    fun i₁ h =>
    let ⟨i, hi, Ne⟩ := Finset.exists_ne_zero_of_sum_ne_zero h
    ⟨i, mem_support_iff.1 hi, Ne⟩
  simpa [Finset.subset_iff, mem_support_iff, Finset.mem_biUnion, sum_apply] using this

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

Goal state before:
pp: α✝ : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α : Type u_7
β : Type u_8
⊢ ∀ (m : R) (x : α ⊕ β →₀ M),
    sumFinsuppAddEquivProdFinsupp.toFun (m • x) = (RingHom.id R) m • sumFinsuppAddEquivProdFinsupp.toFun x

Tactic:
intros
      ext <;>
        simp only [AddEquiv.toFun_eq_coe, Prod.smul_fst, Prod.smul_snd, smul_apply,
          snd_sumFinsuppAddEquivProdFinsupp, fst_sumFinsuppAddEquivProdFinsupp,
          RingHom.id_apply]

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

Goal state before:
pp: α✝ : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α : Type u_7
β : Type u_8
⊢ ∀ (m : R) (x : α ⊕ β →₀ M),
    sumFinsuppAddEquivProdFinsupp.toFun (m • x) = (RingHom.id R) m • sumFinsuppAddEquivProdFinsupp.toFun x

Tactic:
by
      intros
      ext <;>
        simp only [AddEquiv.toFun_eq_coe, Prod.smul_fst, Prod.smul_snd, smul_apply,
          snd_sumFinsuppAddEquivProdFinsupp, fst_sumFinsuppAddEquivProdFinsupp,
          RingHom.id_apply]

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

Goal state before:
pp: case refine_2
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
h : ∀ (i : ι), Function.Surjective (f i)
x : Π₀ (i : ι), β₂ i
⊢ ∃ a, mapRange f hf a = x

Tactic:
obtain ⟨x, s, hs⟩ := x

Goal state after:
case refine_2.mk
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
h : ∀ (i : ι), Function.Surjective (f i)
x : (i : ι) → β₂ i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ x i = 0 }
s : Multiset ι
hs : ∀ (i : ι), i ∈ s ∨ x i = 0
⊢ ∃ a, mapRange f hf a = { toFun := x, support' := Quot.mk ⇑trueSetoid ⟨s, hs⟩ }
Module: Mathlib.Data.Fin.Tuple.Reflection

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
n : ℕ
a : Fin (n + 2) → α
⊢ prod a = ∏ i, a i

Tactic:
Fin.prod_univ_castSucc,

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
a : Fin (n + 2) → α
⊢ prod a = (∏ i, a i.castSucc) * a (Fin.last (n + 1))
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : ι → Type u_5
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
m : Π₀ (i : ι), M i
x✝ : m ∈ ⊤
⊢ m ∈ ⨆ i, (lsingle i).range

Tactic:
← LinearMap.id_apply (R := R) m,

Goal state after:
ι : Type u_1
R : Type u_3
M : ι → Type u_5
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
m : Π₀ (i : ι), M i
x✝ : m ∈ ⊤
⊢ LinearMap.id m ∈ ⨆ i, (lsingle i).range
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
f : ι → M
hij : i ≠ j
⊢ LinearIndepOn R f {i, j} ↔ ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0

Tactic:
rw [linearIndepOn_iff'']
  refine ⟨fun h c d hcd ↦ ?_, fun h t g ht hg0 h0 ↦ ?_⟩
  · specialize h {i, j} (Pi.single i c + Pi.single j d)
    simpa +contextual [Finset.sum_pair, Pi.single_apply, hij, hij.symm, hcd] using h
  have ht' : t ⊆ {i, j} := by simpa [← Finset.coe_subset]
  rw [Finset.sum_subset ht', Finset.sum_pair hij] at h0
  · obtain ⟨hi0, hj0⟩ := h _ _ h0
    exact fun k hkt ↦ Or.elim (ht hkt) (fun h ↦ h ▸ hi0) (fun h ↦ h ▸ hj0)
  simp +contextual [hg0]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
⊢ iSupIndep p ↔ ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0

Tactic:
by
  classical
  simp_rw [iSupIndep_def, Submodule.disjoint_def]
  constructor
  · intro h s v hv hv0 i hi
    apply h _ _ (hv i hi)
    rw [← s.add_sum_erase _ hi, add_eq_zero_iff_neg_eq] at hv0
    rw [← Submodule.neg_mem_iff, hv0]
    exact SetLike.le_def.mp (biSup_mono <| by grind) (Submodule.sum_mem_biSup <| by grind)
  · intro h i x hx hsup
    obtain ⟨f, hf, rfl⟩ := (Submodule.mem_iSup_iff_exists_finsupp ..).mp hsup
    contrapose! h
    use insert i f.support, fun j ↦ if j = i then -f.sum fun _ x ↦ x else f j
    refine ⟨fun j hj ↦ ?_, ?_, by grind⟩
    · beta_reduce
      split_ifs with h
      · exact (p j).neg_mem (h ▸ hx)
      · simpa [h] using hf j
    · specialize hf i
      simp at hf
      grind [Finsupp.sum, Finset.sum_congr]

Goal state after:
Module: Mathlib.Tactic.Module

Goal state before:
pp: S : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring R
inst✝⁴ : Algebra S R
inst✝³ : AddMonoid M
inst✝² : SMul S M
inst✝¹ : MulAction R M
inst✝ : IsScalarTower S R M
l : NF S M
⊢ (algebraMap R l).eval = l.eval

Tactic:
simp only [NF.eval, algebraMap, map_map]
  congr
  ext
  simp [IsScalarTower.algebraMap_smul]

Goal state after:
Module: Mathlib.Algebra.Module.BigOperators

Goal state before:
pp: case cons
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
t : Multiset M
a : R
s : Multiset R
ih : s.sum • t.sum = (map (fun p ↦ p.1 • p.2) (s ×ˢ t)).sum
⊢ (a ::ₘ s).sum • t.sum = (map (fun p ↦ p.1 • p.2) ((a ::ₘ s) ×ˢ t)).sum

Tactic:
| cons a s ih =>

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

Goal state before:
pp: K : Type u_6
M : Type u_7
L : Type u_8
inst✝⁵ : CommSemiring K
inst✝⁴ : Semiring M
inst✝³ : Algebra K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
⊢ LinearIndependent L AlgHom.toLinearMap

Tactic:
apply LinearIndependent.of_comp (LinearMap.ltoFun K M L L)

Goal state after:
K : Type u_6
M : Type u_7
L : Type u_8
inst✝⁵ : CommSemiring K
inst✝⁴ : Semiring M
inst✝³ : Algebra K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
⊢ LinearIndependent L (⇑(ltoFun K M L L) ∘ AlgHom.toLinearMap)
Module: Mathlib.Algebra.MonoidAlgebra.Module

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝¹ : Semiring R
inst✝ : Nontrivial R
m : M
s : Set M
⊢ single m 1 ∈ Submodule.span R ((fun x ↦ single x 1) '' s) ↔ m ∈ s

Tactic:
by
  refine (Set.mem_image_equiv (f := (coeffLinearEquiv R).toEquiv)).symm.trans ?_
  change _ ∈ (Submodule.span R _).map (coeffLinearEquiv R).toLinearMap ↔ _
  simp [Submodule.map_span, ← Set.image_comp, Finsupp.single_mem_span_single]

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

Goal state before:
pp: case h.mp
α : Type u_1
inst✝ : Monoid α
a : α
n : ℕ
f : Fin n → Set α
⊢ (∃ f_1, (List.ofFn fun i ↦ ↑(f_1 i)).prod = a) → ∃ x, (List.ofFn ((fun x ↦ ↑x.snd) ∘ x)).prod = a ∧ Sigma.fst ∘ x = f

pp: case h.mpr
α : Type u_1
inst✝ : Monoid α
a : α
n : ℕ
f : Fin n → Set α
⊢ (∃ x, (List.ofFn ((fun x ↦ ↑x.snd) ∘ x)).prod = a ∧ Sigma.fst ∘ x = f) → ∃ f_1, (List.ofFn fun i ↦ ↑(f_1 i)).prod = a

Tactic:
· rintro ⟨fi, rfl⟩
    exact ⟨fun i ↦ ⟨_, fi i⟩, rfl, rfl⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
inst✝ : DecidableEq α
hf : Injective2 f
⊢ image2 f (↑s ∩ ↑s') ↑t = image2 f ↑s ↑t ∩ image2 f ↑s' ↑t

Tactic:
exact image2_inter_left hf

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

Goal state before:
pp: G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
⊢ {ab | ab.1 ∈ A ∧ ab.2 ∈ B ∧ ab.1 * ab.2 = a0 * b0}.Subsingleton

Tactic:
by
  rintro ⟨x1, y1⟩ (hx : x1 ∈ A ∧ y1 ∈ B ∧ x1 * y1 = a0 * b0) ⟨x2, y2⟩
    (hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = a0 * b0)
  rcases h hx.1 hx.2.1 hx.2.2 with ⟨rfl, rfl⟩
  rcases h hy.1 hy.2.1 hy.2.2 with ⟨rfl, rfl⟩
  rfl

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case zero
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ ↑(npowRec 0 s) = ↑s ^ 0

Tactic:
npowRec,

Goal state after:
case zero
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ ↑1 = ↑s ^ 0
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case zero
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ ↑(npowRec 0 s) = ↑s ^ 0

Tactic:
rw [npowRec, pow_zero, coe_one]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case succ
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
ih : ↑(npowRec n s) = ↑s ^ n
⊢ ↑(npowRec (n + 1) s) = ↑s ^ (n + 1)

Tactic:
npowRec,

Goal state after:
case succ
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
ih : ↑(npowRec n s) = ↑s ^ n
⊢ ↑(npowRec n s * s) = ↑s ^ (n + 1)
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
⊢ {i}ᶜ.orderEmbOfFin h = RelEmbedding.trans (Fin.castOrderIso ⋯).toOrderEmbedding i.succAboveOrderEmb

Tactic:
by
  apply DFunLike.coe_injective
  rw [eq_comm]
  convert!
    orderEmbOfFin_unique _ (fun x ↦ ?_) ((Fin.strictMono_succAbove _).comp (Fin.cast_strictMono _))
  · simp
  · simp [← h, card_compl]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
⊢ IsUnit s → ∃ a, s = {a} ∧ IsUnit a

pp: case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
⊢ (∃ a, s = {a} ∧ IsUnit a) → IsUnit s

Tactic:
· rintro ⟨u, rfl⟩
    obtain ⟨a, b, ha, hb, h⟩ := Finset.mul_eq_one_iff.1 u.mul_inv
    refine ⟨a, ha, ⟨a, b, h, singleton_injective ?_⟩, rfl⟩
    rw [← singleton_mul_singleton, ← ha, ← hb]
    exact u.inv_mul

Goal state after:
case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
⊢ (∃ a, s = {a} ∧ IsUnit a) → IsUnit s
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
b : α
⊢ preimage 1 (fun x ↦ x * b) ⋯ = {b⁻¹}

Tactic:
by
  classical rw [← image_mul_right', image_one, one_mul]

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

Goal state before:
pp: case neg
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
d1 : G
hd1 : d1 ∈ D
c2 : G
hc2 : c2 ∈ C
hc1 : 1 ∈ C
hd2 : 1 ∈ D
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⁻¹ * 1 * (1 * c2⁻¹) → a = d1⁻¹ * 1 ∧ b = 1 * c2⁻¹
h21 : c2 = 1 ∧ d1 = 1
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d

Tactic:
obtain ⟨rfl, rfl⟩ := h21

Goal state after:
case neg
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
hc1 : 1 ∈ C
hd2 : 1 ∈ D
hc2 : 1 ∈ C
hd1 : 1 ∈ D
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 = 1⁻¹ * 1 * (1 * 1⁻¹) → a = 1⁻¹ * 1 ∧ b = 1 * 1⁻¹
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ Nontrivial R[X]

Tactic:
by
  have h : Nontrivial R[ℕ] := by infer_instance
  rcases h.exists_pair_ne with ⟨x, y, hxy⟩
  refine ⟨⟨⟨x⟩, ⟨y⟩, ?_⟩⟩
  simp [hxy]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Finite R
inst✝ : Module.Finite R M
⊢ Finite M

Tactic:
by
  obtain ⟨n, f, hf⟩ := exists_fin' R M; exact .of_surjective f hf

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: case codisjoint
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x : E
a✝ : x ∈ ⊤
⊢ x ∈ p ⊔ f.ker

Tactic:
rw [mem_sup']

Goal state after:
case codisjoint
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x : E
a✝ : x ∈ ⊤
⊢ ∃ y z, ↑y + ↑z = x
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
p q : Submodule R E
h : IsCompl p q
x : E
⊢ ((p.prodEquivOfIsCompl q h).symm x).1 = 0 ↔ x ∈ q

Tactic:
conv_rhs => rw [← (prodEquivOfIsCompl p q h).apply_symm_apply x]
  rw [coe_prodEquivOfIsCompl', Submodule.add_mem_iff_left _ (Submodule.coe_mem _),
    mem_right_iff_eq_zero_of_disjoint h.disjoint]

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: case a
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
⊢ (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯).range ≤ φ.range ⊔ ψ.range

pp: case a
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
⊢ φ.range ⊔ ψ.range ≤ (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯).range

Tactic:
· apply range_add_le _ _ |>.trans
    gcongr
    all_goals exact range_comp_le_range ..

Goal state after:
case a
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
⊢ φ.range ⊔ ψ.range ≤ (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯).range
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: s : Set ℕ∞
h : s.Infinite
x : ℕ∞
hx : x < ⊤
⊢ ∃ a ∈ s, x < a

Tactic:
cases x with
  | top => simp at hx
  | coe x =>
    contrapose! h
    apply Finite.subset <| Finite.Set.finite_image {n : ℕ | n ≤ x} (fun (n : ℕ) => (n : ℕ∞))
    intro y hy
    specialize h y hy
    have hxt : y < ⊤ := lt_of_le_of_lt h hx
    use y.toNat
    simp [toNat_le_of_le_natCast h, LT.lt.ne_top hxt]

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: case inr.inr
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
d : ℕ∞
h : ∀ (i : ι), a * f i ≤ d
hne : a ≠ 0
hι : Nonempty ι
⊢ a * ⨆ i, f i ≤ d

Tactic:
cases d with

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
a : ℕ∞
inst✝ : Nonempty ι
f : ι → ℕ∞
⊢ (⨆ i, f i) + a = ⨆ i, f i + a

Tactic:
simp [add_comm, add_iSup]

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

Goal state before:
pp: case refine_1.left
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), g (↑l x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ Injective ⇑(f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P)

Tactic:
intro x y e
      simp only [add_apply, coe_comp, comp_apply, fst_apply, snd_apply] at e
      suffices x.2 = y.2 from Prod.ext (hf (by rwa [this, add_left_inj] at e)) this
      simpa [h₁, h₂] using DFunLike.congr_arg g e

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p q : RelSeries r
x : α
hx : (x, p.head) ∈ r
hq : (p.last, q.head) ∈ r
⊢ (p.cons x hx).append q ⋯ = (p.append q hq).cons x ⋯

Tactic:
by
  simp only [cons]
  rw [append_assoc]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
hlenpos : p.length ≠ 0
⊢ ↑p.length ≤ n

Tactic:
let p' := p.eraseLast.snoc a (lt_of_lt_of_le (p.eraseLast_last_rel_last (by simp_all)) hlast)

Goal state after:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
hlenpos : p.length ≠ 0
p' : RelSeries {(a, b) | a < b} := (RelSeries.eraseLast p).snoc a ⋯
⊢ ↑p.length ≤ n
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
⊢ image2 (fun m n ↦ (f m) n) s t ⊆ ↑(map₂ f (span R s) (span R t))

Tactic:
image2_subset_iff

Goal state after:
case a
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
⊢ ∀ x ∈ s, ∀ y ∈ t, (f x) y ∈ ↑(map₂ f (span R s) (span R t))
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case right
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last = q.head
i : Fin q.length
⊢ (Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.natAdd p.length i).castSucc,
      Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.natAdd p.length i).succ) ∈
    r

Tactic:
simpa only [Fin.castSucc_natAdd, Fin.succ_natAdd, Fin.addCases_right] using q.step i

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
x : α
⊢ ⨆ p, ⨆ (_ : RelSeries.last p = x), ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p = f x), ↑p.length

Tactic:
apply iSup₂_le

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
x : α
⊢ ∀ (i : LTSeries α), RelSeries.last i = x → ↑i.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p = f x), ↑p.length
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ⨆ y, ⨆ (_ : y < x), height y + 1 ≤ height x

Tactic:
apply iSup₂_le

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ∀ i < x, height i + 1 ≤ height x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x y : α
hyx : y < x
⊢ ⨆ p, ⨆ (_ : RelSeries.last p = y), ↑p.length + 1 ≤ height x

Tactic:
apply iSup₂_le

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x y : α
hyx : y < x
⊢ ∀ (i : LTSeries α), RelSeries.last i = y → ↑i.length + 1 ≤ height x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
h : ∀ (n : ℕ), ∃ p, RelSeries.last p = x ∧ p.length = n
n : ℕ
p : LTSeries α
hlast : RelSeries.last p = x
hp : p.length = n + 1
⊢ (fun x_1 ↦ (↑x_1).length) ⟨p, hlast⟩ = p.length

Tactic:
by simp [hp]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
h : ∀ (n : ℕ), ∃ p, RelSeries.last p = x ∧ p.length = n
n : ℕ
p : LTSeries α
hlast : RelSeries.last p = x
hp : p.length = n + 1
⊢ n < p.length

Tactic:
by simp [hp]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case e'_2.mp
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
p : LTSeries α
hp : RelSeries.head p = x
hl : p.length = n
⊢ ∃ p, RelSeries.last p = x ∧ p.length = n

Tactic:
use p.reverse

Goal state after:
case h
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
p : LTSeries α
hp : RelSeries.head p = x
hl : p.length = n
⊢ (RelSeries.reverse p).last = x ∧ (RelSeries.reverse p).length = n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case e'_2.mpr
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
p : LTSeries αᵒᵈ
hp : RelSeries.last p = x
hl : p.length = n
⊢ ∃ p, RelSeries.head p = x ∧ p.length = n

Tactic:
use p.reverse

Goal state after:
case h
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
p : LTSeries αᵒᵈ
hp : RelSeries.last p = x
hl : p.length = n
⊢ (RelSeries.reverse p).head = x ∧ (RelSeries.reverse p).length = n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case neg
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hfin : ⊤ ≤ height a
⊢ ∃ x < a, ↑n ≤ height x

Tactic:
simp only [top_le_iff, height_eq_top_iff] at hfin

Goal state after:
case neg
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hfin : ∀ (n : ℕ), ∃ p, RelSeries.last p = a ∧ p.length = n
⊢ ∃ x < a, ↑n ≤ height x