mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: 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
inst✝ : Infinite ι
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : i.Maximal
⊢ Cardinal.lift.{w', w} #ι ≤ Cardinal.lift.{w, w'} #κ

Tactic:
let Φ := fun k : κ => (b.repr (v k)).support
  have w₁ : #ι ≤ #(Set.range Φ) := by
    apply Cardinal.le_range_of_union_finset_eq_univ
    exact union_support_maximal_linearIndependent_eq_range_basis b v i m
  have w₂ : Cardinal.lift.{w'} #(Set.range Φ) ≤ Cardinal.lift.{w} #κ := Cardinal.mk_range_le_lift
  exact (Cardinal.lift_le.mpr w₁).trans w₂

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
s : Finset ι
⊢ Function.Injective (mk s)

Tactic:
intro x

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
s : Finset ι
x : (i : ↑↑s) → β ↑i
⊢ ∀ ⦃a₂ : (i : ↑↑s) → β ↑i⦄, mk s x = mk s a₂ → x = a₂
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
⊢ f.update i b = single i b + erase i f

Tactic:
by
  ext j
  rcases eq_or_ne i j with (rfl | h)
  · simp
  · simp [h, h.symm]

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

Goal state before:
pp: ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
⊢ f.update i b = erase i f + single i b

Tactic:
by
  ext j
  rcases eq_or_ne i j with (rfl | h)
  · simp
  · simp [h, h.symm]

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
s : Finset ι
⊢ Function.LeftInverse (fun f ↦ ⟨mk s fun i ↦ ↑(f i), ⋯⟩) fun x ↦
    match (motive := { f // f.support = s } → (i : ↥s) → { x // x ≠ 0 }) x with
    | ⟨f, hf⟩ => fun x ↦
      match x with
      | ⟨i, hi⟩ => ⟨f i, ⋯⟩

Tactic:
by
    rintro ⟨f, rfl⟩
    ext i
    simpa using Eq.symm

Goal state after:
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: case neg
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
H : ⟨i, a⟩ ≠ ⟨j, b⟩
⊢ (single ⟨i, a⟩ n) ⟨j, b⟩ = 0

Tactic:
classical rw [Finsupp.single_apply, if_neg H]

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

Goal state before:
pp: case neg
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
s : Multiset ι
hf : ∀ (i : ι), i ∈ s ∨ f i = 0
i : ι
a✝ : i ∈ s.toFinset
h : ¬{ toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } i ≠ 0
⊢ (φ i) ({ toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } i) = 0

Tactic:
not_not.mp h,

Goal state after:
case neg
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
s : Multiset ι
hf : ∀ (i : ι), i ∈ s ∨ f i = 0
i : ι
a✝ : i ∈ s.toFinset
h : ¬{ toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } i ≠ 0
⊢ (φ i) 0 = 0
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι₁ : Type u_4
ι₂ : Type u_5
β₁ : ι₁ → Type u_1
β₂ : ι₂ → Type u_2
γ : Type u_3
inst✝⁴ : DecidableEq ι₁
inst✝³ : DecidableEq ι₂
inst✝² : (i : ι₁) → AddZeroClass (β₁ i)
inst✝¹ : (i : ι₂) → AddZeroClass (β₂ i)
inst✝ : AddCommMonoid γ
f₁ : Π₀ (i : ι₁), β₁ i
f₂ : Π₀ (i : ι₂), β₂ i
h : (i : ι₁) → (j : ι₂) → β₁ i →+ β₂ j →+ γ
⊢ (sumAddHom fun i₂ ↦ (sumAddHom fun i₁ ↦ h i₁ i₂) f₁) f₂ =
    (sumAddHom fun i₁ ↦ (sumAddHom fun i₂ ↦ (h i₁ i₂).flip) f₂) f₁

Tactic:
by
  obtain ⟨⟨f₁, s₁, h₁⟩, ⟨f₂, s₂, h₂⟩⟩ := f₁, f₂
  simpa [sumAddHom, sumZeroHom, AddMonoidHom.finsetSum_apply, AddMonoidHom.coe_mk,
      AddMonoidHom.flip_apply, Trunc.lift, toFun_eq_coe, ZeroHom.coe_mk, coe_mk']
    using Finset.sum_comm

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
γ : Type w
α : Type x
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
s : Finset α
g : α → Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_zero : ∀ (i : ι), h i 0 = 1
h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂
⊢ ∏ i ∈ s, (g i).prod h = (∑ i ∈ s, g i).prod h

Tactic:
exact Finset.induction_on s (by simp [prod_zero_index])
        (by simp +contextual [prod_add_index, h_zero, h_add])

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case h.h
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
⊢ μ.support ⊆ s

Tactic:
intro x

Goal state after:
case h.h
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
x : ι
⊢ x ∈ μ.support → x ∈ s
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case h.h
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
⊢ μ.support ⊆ s

Tactic:
intro x
        contrapose
        intro hx
        rw [mem_support_iff, not_ne_iff]
        ext
        rw [coe_zero, ← mem_bot R]
        suffices ⊥ = ⨆ (_ : x ∈ s), p x from this.symm ▸ coe_mem (μ x)
        exact (iSup_neg hx).symm

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case h.hf
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
⊢ ∀ x ∈ s, x ∉ μ.support → (fun x xi ↦ ↑xi) x (μ x) = 0

Tactic:
intro x

Goal state after:
case h.hf
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
x : ι
⊢ x ∈ s → x ∉ μ.support → (fun x xi ↦ ↑xi) x (μ x) = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mpr.refine_2
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
⊢ ∀ x ∈ s, x ∉ (DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩).support → ↑((DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x) = 0

Tactic:
intro x

Goal state after:
case mpr.refine_2
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
x : ι
⊢ x ∈ s → x ∉ (DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩).support → ↑((DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x) = 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
x y : M
⊢ ∀ (x y : M), (∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0) → ∀ (s t : R), s • y + t • x = 0 → s = 0 ∧ t = 0

Tactic:
intro x

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ y x : M
⊢ ∀ (y : M), (∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0) → ∀ (s t : R), s • y + t • x = 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
x y : M
⊢ ∀ (x y : M), (∀ (s t : R), s • x + t • (x + y) = 0 → s = 0 ∧ t = 0) → ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0

Tactic:
intro x

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ y x : M
⊢ ∀ (y : M), (∀ (s t : R), s • x + t • (x + y) = 0 → s = 0 ∧ t = 0) → ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
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
v : ι → M
I : Set ι
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 : ∑ i ∈ f.support, f i • v i = 0
f_ne : f ≠ 0
hIlinind : f i = 0
⊢ f ∈ Finsupp.supported R R I

Tactic:
simp only [Finsupp.mem_supported, hJ] at supp_f ⊢

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
I : Set ι
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
sum_f : ∑ i ∈ f.support, f i • v i = 0
f_ne : f ≠ 0
hIlinind : f i = 0
supp_f : ↑f.support ⊆ I ∪ {i}
⊢ ↑f.support ⊆ I
Module: Mathlib.Algebra.MonoidAlgebra.Module

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Module R S
e : M ≃ N
s : S
m : M
⊢ (mapDomainLinearEquiv R S e) (single m s) = single (e m) s

Tactic:
simp [mapDomainLinearEquiv]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
inst✝⁵ : CommSemiring S
inst✝⁴ : Monoid M
V : Type u_7
inst✝³ : AddCommMonoid V
inst✝² : Module S V
inst✝¹ : Module S[M] V
inst✝ : IsScalarTower S S[M] V
W : Submodule S V
h : ∀ (g : M), ∀ v ∈ W, (of S M) g • v ∈ W
f : S[M]
v : V
hv : v ∈ ↑W
⊢ ∑ x ∈ f.coeff.support, f.coeff x • (of S M) x • v ∈ ↑W

Tactic:
exact Submodule.sum_smul_mem W _ fun g _ => h g v hv

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 t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
⊢ t ⊆ ↑(span K (hs.extend hst))

Tactic:
by
  convert! hs.image_subset_span_image_extend hst <;> simp

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

Goal state before:

Tactic:
(x * y).coeff m = ∑ m₁ ∈ x.coeff.support, ∑ m₂ ∈ y.coeff.support, F (m₁, m₂) := coeff_mul ..
    _ = ∑ p ∈ x.coeff.support ×ˢ y.coeff.support with p.1 * p.2 = m, x.coeff p.1 * y.coeff p.2 := by
      rw [Finset.sum_filter, Finset.sum_product]
    _ = ∑ p ∈ s with p.1 ∈ x.coeff.support ∧ p.2 ∈ y.coeff.support, x.coeff p.1 * y.coeff p.2 := by
      congr! 1; ext; simp only [mem_filter, mem_product, hs, and_comm]
    _ = ∑ p ∈ s, x.coeff p.1 * y.coeff p.2 :=
      sum_subset (filter_subset _ _) fun p hps hp => by
        simp only [mem_filter, mem_support_iff, not_and, Classical.not_not] at hp ⊢
        by_cases h1 : x.coeff p.1 = 0
        · rw [h1, zero_mul]
        · rw [hp hps h1, mul_zero]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
x : α
hx : x ∈ image f univ
⊢ x ∈ s

Tactic:
rcases mem_image.1 hx with ⟨x, _, rfl⟩
    exact hfs x

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
hα : Finite α
β : Type u_2
inst✝ : LinearOrder β
hβ : Infinite β
⊢ Nonempty (α ↪o β)

Tactic:
have := Fintype.ofFinite α

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
hα : Finite α
β : Type u_2
inst✝ : LinearOrder β
hβ : Infinite β
this : Fintype α
⊢ Nonempty (α ↪o β)
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
⊢ Free R' M'

Tactic:
let e₁ : R ≃+* R' := RingHomInvPair.toRingEquiv σ σ'
  let I := Module.Free.ChooseBasisIndex R M
  obtain ⟨e₃ : M ≃ₗ[R] I →₀ R⟩ := Module.Free.chooseBasis R M
  let e : M' ≃+ (I →₀ R') :=
    (e₂.symm.trans e₃).toAddEquiv.trans (Finsupp.mapRange.addEquiv (ι := I) e₁.toAddEquiv)
  have he (x) : e x = Finsupp.mapRange.addEquiv (ι := I) e₁.toAddEquiv (e₃ (e₂.symm x)) := rfl
  let e' : M' ≃ₗ[R'] (I →₀ R') :=
    { __ := e, map_smul' := fun m x ↦ Finsupp.ext fun i ↦ by simp [e₁, he, map_smulₛₗ] }
  exact of_basis (.ofRepr e')

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

Goal state before:
pp: case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
⊢ span R (Set.range fun x ↦ single (u x) 1) ≤ (lmapDomain R R u).range

Tactic:
rw [Submodule.span_le, Set.range_subset_iff]

Goal state after:
case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
⊢ ∀ (y : α), single (u y) 1 ∈ ↑(lmapDomain R R u).range
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
σ : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
φ : M →ₗ[R] N
f : σ → R
⊢ ((lsum R) fun x ↦ f x • φ).range = Set.range f • φ.range

Tactic:
simp_rw [range_eq_map, ← span_single_eq_top, ← span_univ, map_span, set_smul_span]
  congr 1
  aesop (add simp Set.mem_smul)

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

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : End R N
e : M ≃ₗ[R] N
p : Submodule R M
⊢ Submodule.map (↑e) p ∈ f.invtSubmodule ↔ p ∈ (e.symm.conj f).invtSubmodule

Tactic:
simp [← e.map_mem_invtSubmodule_conj_iff]

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
⊢ ⊤ ≤ p ⊔ f.ker

Tactic:
intro x

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
⊢ x ∈ ⊤ → x ∈ p ⊔ f.ker
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case a.refine_2
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
⊢ ↑t2 ⊆ ↑s

Tactic:
intro x

Goal state after:
case a.refine_2
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
⊢ x ∈ ↑t2 → x ∈ ↑s
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case a.refine_2
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 ∈ ↑t2
this : x ∈ span R ↑t2
⊢ x ∈ ↑s

Tactic:
rw [ht2] at this

Goal state after:
case a.refine_2
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 ∈ ↑t2
this : x ∈ s ⊓ f.ker
⊢ x ∈ ↑s
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case a
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
⊢ s ≤ span R (g '' ↑t1) ⊔ span R ↑t2

Tactic:
intro x

Goal state after:
case a
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
⊢ x ∈ s → x ∈ span R (g '' ↑t1) ⊔ span R ↑t2
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: M : Type u_2
N : Type u_4
P : Type u_6
P' : Type u_7
f : M → N
g : N → P
g' : P → P'
inst✝¹ : One P
inst✝ : One P'
mulExact : MulExact f g
inj : Injective g'
h0 : g' 1 = 1
⊢ MulExact f (g' ∘ g)

Tactic:
intro x

Goal state after:
M : Type u_2
N : Type u_4
P : Type u_6
P' : Type u_7
f : M → N
g : N → P
g' : P → P'
inst✝¹ : One P
inst✝ : One P'
mulExact : MulExact f g
inj : Injective g'
h0 : g' 1 = 1
x : N
⊢ (g' ∘ g) x = 1 ↔ x ∈ Set.range f
Module: Mathlib.Data.ENat.Lattice

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

Tactic:
intro x

Goal state after:
s : Set ℕ∞
h : s.Infinite
x : ℕ∞
⊢ x < ⊤ → ∃ a ∈ s, x < a
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: s : Set ℕ∞
a : ℕ∞
⊢ sSup s * a = ⨆ b ∈ s, b * a

Tactic:
simp_rw [mul_comm, mul_sSup]

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

Goal state after:
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
x : M × P
⊢ ∀ ⦃a₂ : M × P⦄, (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) x = (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) a₂ → x = a₂
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
R : SetRel α β
⊢ R ○ Set.univ = {(a, _c) | a ∈ R.dom}

Tactic:
by
  aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
S : SetRel β γ
⊢ Set.univ ○ S = {(_b, c) | c ∈ S.cod}

Tactic:
by
  aesop

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

Goal state before:
pp: case refine_1.right
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
⊢ Surjective ⇑(f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P)

Tactic:
intro x

Goal state after:
case refine_1.right
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
x : N
⊢ ∃ a, (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) a = x
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
ht : t.Nonempty
⊢ preimage Set.univ t = Set.univ

Tactic:
by
  aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α ≃ β
⊢ Function.graph ⇑f.symm = (Function.graph ⇑f).inv

Tactic:
by
  aesop

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case inr.inr
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length) < i
x : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.succ
⊢ (Fin.append p.toFun q.toFun x, Fin.append p.toFun q.toFun y) ∈ r

Tactic:
have hx : x = Fin.natAdd _ ⟨i - (p.length + 1), Nat.sub_lt_left_of_lt_add hi <|
          i.2.trans <| by lia⟩ := by
        ext; dsimp [x, y]; rw [Nat.add_sub_cancel']; exact hi

Goal state after:
case inr.inr
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length) < i
x : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length + 1) ⟨↑i - (p.length + 1), ⋯⟩
⊢ (Fin.append p.toFun q.toFun x, Fin.append p.toFun q.toFun y) ∈ r
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✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
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
hg : Surjective ⇑g
l : { l // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ↑l (f x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ Injective ⇑((↑l).prod g)

Tactic:
intro x

Goal state after:
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✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
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
hg : Surjective ⇑g
l : { l // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ↑l (f x) = x
h₂ : ∀ (x : M), g (f x) = 0
x : N
⊢ ∀ ⦃a₂ : N⦄, ((↑l).prod g) x = ((↑l).prod g) a₂ → x = a₂