mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f : Dual R M₁
⊢ (dualMap f).range = R ∙ f

Tactic:
by
  ext m
  rw [Submodule.mem_span_singleton]
  refine ⟨fun ⟨r, hr⟩ ↦ ⟨r 1, ?_⟩, fun ⟨r, hr⟩ ↦ ⟨r • LinearMap.id, ?_⟩⟩
  · ext; simp [dualMap_apply', ← hr]
  · ext; simp [dualMap_apply', ← hr]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : M ≃ₗ[R] N
ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := e.symm.dualMap.dualMap
m : N
f : Dual R N
⊢ ((Dual.eval R N) m) f = ((↑ed.symm ∘ₗ Dual.eval R M ∘ₗ ↑e.symm) m) f

Tactic:
exact DFunLike.congr_arg f (e.apply_symm_apply m).symm

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

Goal state before:
pp: ι : Type u'
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'
f : M →ₗ[R] M'
inj : Injective ⇑f
m : ι → Submodule R M
ind : ∀ (i : ι), m i ⊓ ⨆ j, ⨆ (_ : j ≠ i), m j ≤ ⊥
i : ι
x : M
hxi : x ∈ ↑(m i)
hx : f x ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), map f (m j))
⊢ f 0 ∈ ⊥

pp: ι : Type u'
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'
f : M →ₗ[R] M'
inj : Injective ⇑f
m : ι → Submodule R M
ind : ∀ (i : ι), m i ⊓ ⨆ j, ⨆ (_ : j ≠ i), m j ≤ ⊥
i : ι
x : M
hxi : x ∈ ↑(m i)
hx : f x ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), map f (m j))
⊢ x ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), m j)

Tactic:
· simp

Goal state after:
ι : Type u'
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'
f : M →ₗ[R] M'
inj : Injective ⇑f
m : ι → Submodule R M
ind : ∀ (i : ι), m i ⊓ ⨆ j, ⨆ (_ : j ≠ i), m j ≤ ⊥
i : ι
x : M
hxi : x ∈ ↑(m i)
hx : f x ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), map f (m j))
⊢ x ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), m j)
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
h : ∀ (i : ι), ∀ x ∈ p i, x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j → x = 0
s : Finset ι
v : ι → N
hv : ∀ i ∈ s, v i ∈ p i
i : ι
hv0 : -v i = ∑ x ∈ s.erase i, v x
hi : i ∈ s
⊢ ∀ i_1 ∈ s.erase i, i_1 ≠ i

Tactic:
by grind

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
h : ∀ (i : ι), ∀ x ∈ p i, x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j → x = 0
s : Finset ι
v : ι → N
hv : ∀ i ∈ s, v i ∈ p i
i : ι
hv0 : -v i = ∑ x ∈ s.erase i, v x
hi : i ∈ s
⊢ ∀ i_1 ∈ s.erase i, v i_1 ∈ p i_1

Tactic:
by grind

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

Goal state before:
pp: case refine_1
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 • u • x + t • u • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • x + t • y = 0
⊢ s = 0 ∧ t = 0

pp: case refine_2
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
⊢ s = 0 ∧ t = 0

Tactic:
· exact h s t (by rw [← smul_comm u s, ← smul_comm u t, ← smul_add, hst, smul_zero])

Goal state after:
case refine_2
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
⊢ s = 0 ∧ t = 0
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
i : ι
f : ι →₀ N
hf : ∀ (i_1 : ι), f i_1 ∈ ⨆ (_ : i_1 ≠ i), p i_1
hx : (f.sum fun _i xi ↦ xi) ∈ p i
hsup : (f.sum fun _i xi ↦ xi) ∈ ⨆ j, ⨆ (_ : j ≠ i), p j
h : (f.sum fun _i xi ↦ xi) ≠ 0
⊢ ∃ i_1 ∈ insert i f.support, (fun j ↦ if j = i then -f.sum fun x x_1 ↦ x_1 else f j) i_1 ≠ 0

Tactic:
by grind

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

Goal state before:
pp: ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
s : Set ι
x : ι
hs : LinearIndepOn K v s
hx : v x ∉ span K (v '' s)
x0 : v x ≠ 0
⊢ Disjoint (span K (v '' s)) (span K (v '' {x}))

Tactic:
image_singleton,

Goal state after:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
s : Set ι
x : ι
hs : LinearIndepOn K v s
hx : v x ∉ span K (v '' s)
x0 : v x ≠ 0
⊢ Disjoint (span K (v '' s)) (K ∙ v x)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_6
K : Type u_7
M : Type u_8
inst✝⁷ : CommRing R
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R K
inst✝³ : Module K M
inst✝² : Module R M
inst✝¹ : IsScalarTower R K M
inst✝ : FaithfulSMul R K
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
x : M
hx : x ∉ span K (range v)
c : R
y : M
hcy : y ∈ span R (range v)
heq : c • x + y = 0
hc : ¬c = 0
hc' : (algebraMap R K) c ≠ 0
⊢ x ∈ span K (range v)

Tactic:
rw [← algebraMap_smul K c x] at heq

Goal state after:
R : Type u_6
K : Type u_7
M : Type u_8
inst✝⁷ : CommRing R
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R K
inst✝³ : Module K M
inst✝² : Module R M
inst✝¹ : IsScalarTower R K M
inst✝ : FaithfulSMul R K
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
x : M
hx : x ∉ span K (range v)
c : R
y : M
hcy : y ∈ span R (range v)
heq : (algebraMap R K) c • x + y = 0
hc : ¬c = 0
hc' : (algebraMap R K) c ≠ 0
⊢ x ∈ span K (range v)
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:
by
  let l := s.sort
  apply le_antisymm
  · have : s.min' H ∈ l := (s.mem_sort (· ≤ ·)).mpr (s.min'_mem H)
    obtain ⟨i, hi⟩ : ∃ i, l.get i = s.min' H := List.mem_iff_get.1 this
    rw [← hi]
    exact (s.pairwise_sort (· ≤ ·)).rel_get_of_le (Nat.zero_le i)
  · have : l.get ⟨0, h⟩ ∈ s := (Finset.mem_sort (α := α) (· ≤ ·)).1 (List.get_mem l _)
    exact s.min'_le _ this

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

Goal state before:
pp: case mp.inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ (s ^ 0).Nonempty

Tactic:
· simp

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

Goal state before:
pp: case a
α : 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
this : s.max' H ∈ l
i : Fin l.length
hi : l.get i = s.max' H
⊢ l.get i ≤ (s.sort fun a b ↦ a ≤ b)[(s.sort fun a b ↦ a ≤ b).length - 1]

Tactic:
exact (s.pairwise_sort (· ≤ ·)).rel_get_of_le (Nat.le_sub_one_of_lt i.prop)

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

Goal state before:
pp: case convert_3
n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
x : Fin k
⊢ (i.succAbove ∘ Fin.cast ?convert_7) x ∈ {i}ᶜ

pp: case convert_7
n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
⊢ k = n

Tactic:
· simp

Goal state after:
case convert_7
n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
⊢ k = n
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
b1 : G
hb1 : b1 ∈ B
a1 : G
ha1 : a1 ∈ A
h1 : b1 * a1 ∈ B * A
b2 : G
hb2 : b2 ∈ B
a2 : G
ha2 : a2 ∈ A
h2 : b2 * a2 ∈ B * A
hu : UniqueMul (B * A) (B * A) (b1 * a1) (b2 * a2)
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a1 * b2
⊢ b1 * (a1 * b2 * a2) = b1 * a1 * (b2 * a2)

Tactic:
mul_assoc a1,

Goal state after:
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
b1 : G
hb1 : b1 ∈ B
a1 : G
ha1 : a1 ∈ A
h1 : b1 * a1 ∈ B * A
b2 : G
hb2 : b2 ∈ B
a2 : G
ha2 : a2 ∈ A
h2 : b2 * a2 ∈ B * A
hu : UniqueMul (B * A) (B * A) (b1 * a1) (b2 * a2)
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a1 * b2
⊢ b1 * (a1 * (b2 * a2)) = b1 * a1 * (b2 * a2)
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case mp.inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
⊢ (s ^ 0).Nonempty

Tactic:
· simp

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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
m : M
x✝ : ∃ s, m ∈ ⨆ i ∈ s, ↑i
s : Finset (Subtype (Membership.mem S))
hs : m ∈ ⨆ i ∈ s, ↑i
⊢ ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ S) s) ⊆ S

pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
m : M
x✝ : ∃ s, m ∈ ⨆ i ∈ s, ↑i
s : Finset (Subtype (Membership.mem S))
hs : m ∈ ⨆ i ∈ s, ↑i
⊢ m ∈ ⨆ i ∈ Finset.map (Function.Embedding.subtype fun x ↦ x ∈ S) s, i

pp: case refine_3
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
m : M
x✝ : ∃ s, ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i
s : Finset (Submodule R M)
hsS : ↑s ⊆ S
hs : m ∈ ⨆ i ∈ s, i
⊢ m ∈ ⨆ i ∈ s.preimage Subtype.val ⋯, ↑i

Tactic:
· simp

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
m : M
x✝ : ∃ s, m ∈ ⨆ i ∈ s, ↑i
s : Finset (Subtype (Membership.mem S))
hs : m ∈ ⨆ i ∈ s, ↑i
⊢ m ∈ ⨆ i ∈ Finset.map (Function.Embedding.subtype fun x ↦ x ∈ S) s, i

case refine_3
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
m : M
x✝ : ∃ s, ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i
s : Finset (Submodule R M)
hsS : ↑s ⊆ S
hs : m ∈ ⨆ i ∈ s, i
⊢ m ∈ ⨆ i ∈ s.preimage Subtype.val ⋯, ↑i
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ (monomial n) 1 = X ^ n

Tactic:
induction n with
  | zero => simp
  | succ n ih => rw [pow_succ, ← ih, ← monomial_one_one_eq_X, monomial_mul_monomial, mul_one]

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

Goal state before:
pp: 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
hs1 : (map f s).FG
hs2 : (s ⊓ f.ker).FG
this : DecidableEq R
⊢ s.FG

Tactic:
have := Classical.decEq M

Goal state after:
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
hs1 : (map f s).FG
hs2 : (s ⊓ f.ker).FG
this✝ : DecidableEq R
this : DecidableEq M
⊢ s.FG
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case hs1
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hf1 : f.ker.FG
hf2 : g.ker.FG
hsur : Surjective ⇑f
⊢ (f.range ⊓ g.ker).FG

Tactic:
LinearMap.range_eq_top.2 hsur,

Goal state after:
case hs1
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hf1 : f.ker.FG
hf2 : g.ker.FG
hsur : Surjective ⇑f
⊢ (⊤ ⊓ g.ker).FG
Module: Mathlib.RingTheory.Finiteness.Finsupp

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

Tactic:
simp [LinearMap.exact_iff.1 h_exact]

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

Goal state before:
pp: case inl
ι : Sort u_1
f : ι → ℕ
h✝ : IsEmpty ι
⊢ (⨅ i, ↑(f i)).toNat = ⨅ i, f i

pp: case inr
ι : Sort u_1
f : ι → ℕ
h✝ : Nonempty ι
⊢ (⨅ i, ↑(f i)).toNat = ⨅ i, f i

Tactic:
· simp

Goal state after:
case inr
ι : Sort u_1
f : ι → ℕ
h✝ : Nonempty ι
⊢ (⨅ i, ↑(f i)).toNat = ⨅ i, f i
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: case inl
ι : Sort u_2
f : ι → ℕ∞
d : ℕ∞
h : ∀ (i : ι), 0 * f i ≤ d
⊢ 0 * ⨆ i, f i ≤ d

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

Tactic:
· simp

Goal state after:
case inr
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
d : ℕ∞
h : ∀ (i : ι), a * f i ≤ d
hne : a ≠ 0
⊢ a * ⨆ i, f i ≤ d
Module: Mathlib.Data.ENat.Lattice

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

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:
· simp

Goal state after:
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
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: case inl
ι : Sort u_2
inst✝ : Nonempty ι
f : ι → ℕ∞
⊢ ⊤ + ⨆ i, f i = ⨆ i, ⊤ + f i

pp: case inr
ι : Sort u_2
a : ℕ∞
inst✝ : Nonempty ι
f : ι → ℕ∞
ha : a ≠ ⊤
⊢ a + ⨆ i, f i = ⨆ i, a + f i

Tactic:
· simp

Goal state after:
case inr
ι : Sort u_2
a : ℕ∞
inst✝ : Nonempty ι
f : ι → ℕ∞
ha : a ≠ ⊤
⊢ a + ⨆ i, f i = ⨆ i, a + f i
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: case inl
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : IsEmpty ι
⊢ iSup f + iSup g = ⨆ i, f i + g i

pp: case inr
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
⊢ iSup f + iSup g = ⨆ i, f i + g i

Tactic:
· simp

Goal state after:
case inr
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
⊢ iSup f + iSup g = ⨆ i, f i + g i
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
x : ↑{x | x ≠ [] ∧ List.IsChain (fun x1 x2 ↦ (x1, x2) ∈ r) x}
⊢ (↑((fun x ↦ ⟨x.toList, ⋯⟩) ((fun x ↦ fromListIsChain ↑x ⋯ ⋯) x))).length = (↑x).length

Tactic:
have := Nat.succ_pred_eq_of_pos <| List.length_pos_iff.mpr x.2.1

Goal state after:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
x : ↑{x | x ≠ [] ∧ List.IsChain (fun x1 x2 ↦ (x1, x2) ∈ r) x}
this : (↑x).length.pred.succ = (↑x).length
⊢ (↑((fun x ↦ ⟨x.toList, ⋯⟩) ((fun x ↦ fromListIsChain ↑x ⋯ ⋯) x))).length = (↑x).length
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
s : RelSeries r
inst✝ : r.IsIrrefl
⊢ s.length = 0 ↔ {x | x ∈ s}.Subsingleton

Tactic:
by
  rw [← not_ne_iff, length_ne_zero, Set.not_nontrivial_iff]

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
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
have : UniqueMul A B a0 b0 := by
      intro a b ha hb he
      obtain hl | rfl | hl := lt_trichotomy b b0
      · exact ((he0 ▸ he ▸ mul_lt_mul_right hl a).not_ge <| le_max' _ _ <| mul_mem_mul ha hb0).elim
      · exact ⟨mul_right_cancel he, rfl⟩
      · exact ((he0 ▸ mul_lt_mul_right hl a0).not_ge <| le_max' _ _ <| mul_mem_mul ha0 hb).elim

Goal state after:
G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case refine_1
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 }
⊢ Bijective ⇑((↑l).prod g)

Tactic:
have h₁ : ∀ x, l.1 (f x) = x := LinearMap.congr_fun l.2
    have h₂ : ∀ x, g (f x) = 0 := congr_fun h.comp_eq_zero
    constructor
    · intro x y e
      simp only [LinearMap.prod_apply, Function.prod_apply, Prod.mk.injEq] at e
      obtain ⟨z, hz⟩ := (h (x - y)).mp (by simpa [sub_eq_zero] using e.2)
      rw [← sub_eq_zero, ← hz, ← h₁ z, hz, map_sub, e.1, sub_self, map_zero]
    · rintro ⟨x, y⟩
      obtain ⟨y, rfl⟩ := hg y
      refine ⟨f x + y - f (l.1 y), by ext <;> simp [h₁, h₂]⟩

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

Goal state before:
pp: R : Type u
S : Type u₁
T : Type u_1
inst✝⁸ : Monoid R
inst✝⁷ : Monoid S
inst✝⁶ : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : DistribMulAction S B
inst✝¹ : NonUnitalNonAssocSemiring C
inst✝ : DistribMulAction T C
⊢ Function.Injective fun f ↦ f.toFun

Tactic:
rintro ⟨⟨⟨f, _⟩, _⟩, _⟩ ⟨⟨⟨g, _⟩, _⟩, _⟩ h

Goal state after:
R : Type u
S : Type u₁
T : Type u_1
inst✝⁸ : Monoid R
inst✝⁷ : Monoid S
inst✝⁶ : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : DistribMulAction S B
inst✝¹ : NonUnitalNonAssocSemiring C
inst✝ : DistribMulAction T C
f : A → B
map_smul'✝¹ : ∀ (m : R) (x : A), f (m • x) = φ m • f x
map_zero'✝¹ : { toFun := f, map_smul' := map_smul'✝¹ }.toFun 0 = 0
map_add'✝¹ :
  ∀ (x y : A),
    { toFun := f, map_smul' := map_smul'✝¹ }.toFun (x + y) =
      { toFun := f, map_smul' := map_smul'✝¹ }.toFun x + { toFun := f, map_smul' := map_smul'✝¹ }.toFun y
map_mul'✝¹ :
  ∀ (x y : A),
    { toFun := f, map_smul' := map_smul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }.toFun (x * y) =
      { toFun := f, map_smul' := map_smul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }.toFun x *
        { toFun := f, map_smul' := map_smul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }.toFun y
g : A → B
map_smul'✝ : ∀ (m : R) (x : A), g (m • x) = φ m • g x
map_zero'✝ : { toFun := g, map_smul' := map_smul'✝ }.toFun 0 = 0
map_add'✝ :
  ∀ (x y : A),
    { toFun := g, map_smul' := map_smul'✝ }.toFun (x + y) =
      { toFun := g, map_smul' := map_smul'✝ }.toFun x + { toFun := g, map_smul' := map_smul'✝ }.toFun y
map_mul'✝ :
  ∀ (x y : A),
    { toFun := g, map_smul' := map_smul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun (x * y) =
      { toFun := g, map_smul' := map_smul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun x *
        { toFun := g, map_smul' := map_smul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun y
h :
  (fun f ↦ f.toFun)
      { toFun := f, map_smul' := map_smul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹,
        map_mul' := map_mul'✝¹ } =
    (fun f ↦ f.toFun)
      { toFun := g, map_smul' := map_smul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝, map_mul' := map_mul'✝ }
⊢ { toFun := f, map_smul' := map_smul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹, map_mul' := map_mul'✝¹ } =
    { toFun := g, map_smul' := map_smul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝, map_mul' := map_mul'✝ }
Module: Mathlib.Algebra.Algebra.NonUnitalHom

Goal state before:
pp: R : Type u
S : Type u₁
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
φ : R →* S
A : Type v
B : Type w
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : DistribMulAction S B
⊢ Function.Injective DFunLike.coe

Tactic:
rintro ⟨⟨⟨f, _⟩, _⟩, _⟩ ⟨⟨⟨g, _⟩, _⟩, _⟩ h

Goal state after:
R : Type u
S : Type u₁
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
φ : R →* S
A : Type v
B : Type w
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : DistribMulAction S B
f : A → B
map_smul'✝¹ : ∀ (m : R) (x : A), f (m • x) = φ m • f x
map_zero'✝¹ : { toFun := f, map_smul' := map_smul'✝¹ }.toFun 0 = 0
map_add'✝¹ :
  ∀ (x y : A),
    { toFun := f, map_smul' := map_smul'✝¹ }.toFun (x + y) =
      { toFun := f, map_smul' := map_smul'✝¹ }.toFun x + { toFun := f, map_smul' := map_smul'✝¹ }.toFun y
map_mul'✝¹ :
  ∀ (x y : A),
    { toFun := f, map_smul' := map_smul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }.toFun (x * y) =
      { toFun := f, map_smul' := map_smul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }.toFun x *
        { toFun := f, map_smul' := map_smul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }.toFun y
g : A → B
map_smul'✝ : ∀ (m : R) (x : A), g (m • x) = φ m • g x
map_zero'✝ : { toFun := g, map_smul' := map_smul'✝ }.toFun 0 = 0
map_add'✝ :
  ∀ (x y : A),
    { toFun := g, map_smul' := map_smul'✝ }.toFun (x + y) =
      { toFun := g, map_smul' := map_smul'✝ }.toFun x + { toFun := g, map_smul' := map_smul'✝ }.toFun y
map_mul'✝ :
  ∀ (x y : A),
    { toFun := g, map_smul' := map_smul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun (x * y) =
      { toFun := g, map_smul' := map_smul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun x *
        { toFun := g, map_smul' := map_smul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun y
h :
  ⇑{ toFun := f, map_smul' := map_smul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹, map_mul' := map_mul'✝¹ } =
    ⇑{ toFun := g, map_smul' := map_smul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝, map_mul' := map_mul'✝ }
⊢ { toFun := f, map_smul' := map_smul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹, map_mul' := map_mul'✝¹ } =
    { toFun := g, map_smul' := map_smul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝, map_mul' := map_mul'✝ }
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring 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 : f.range ≤ g.ker
hg : Function.Surjective ⇑g
x₃ : P
⊢ ∃ a, (f.range.liftQ g h) a = x₃

Tactic:
obtain ⟨x₂, rfl⟩ := hg x₃

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring 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 : f.range ≤ g.ker
hg : Function.Surjective ⇑g
x₂ : N
⊢ ∃ a, (f.range.liftQ g h) a = g x₂