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

Goal state before:
pp: case mk.mk.e_a
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
f : (i : ι) → β i
support'✝¹ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
g : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ g i = 0 }
sg : Multiset ι
hg : ∀ (i : ι), i ∈ sg ∨ g i = 0
⊢ ∑ x ∈ (sf + sg).toFinset, (φ x) (g x) = ∑ x ∈ sg.toFinset, (φ x) (g x)

Tactic:
· refine (Finset.sum_subset ?_ ?_).symm
      · intro i
        simp only [Multiset.mem_toFinset, Multiset.mem_add]
        exact Or.inr
      · intro i _ H2
        simp only [Multiset.mem_toFinset] at H2
        rw [(hg i).resolve_left H2, map_zero]

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

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁸ : CommSemiring K
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module K V
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
r : R
hr : IsRegular r
m₁ m₂ : M
hm : (fun x ↦ r • x) m₁ = (fun x ↦ r • x) m₂
⊢ (Dual.eval R M) m₁ = (Dual.eval R M) m₂

Tactic:
ext n; simpa [hr.1.eq_iff] using congr(n $hm)

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Submodule R N
inst✝ : (i : ι) → (x : ↥(p i)) → Decidable (x ≠ 0)
x : N
⊢ x ∈ iSup p ↔ ∃ f, (f.sum fun x xi ↦ ↑xi) = x

Tactic:
by
  rw [mem_iSup_iff_exists_dfinsupp]
  simp_rw [DFinsupp.lsum_apply_apply, DFinsupp.sumAddHom_apply,
    LinearMap.toAddMonoidHom_coe, coe_subtype]

Goal state after:
Module: Mathlib.LinearAlgebra.Isomorphisms

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ Function.Surjective ⇑(quotientInfToSupQuotient p p')

Tactic:
rw [← range_eq_top, quotientInfToSupQuotient, range_liftQ, eq_top_iff']

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ ∀ (x : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p'), x ∈ (subToSupQuotient p p').range
Module: Mathlib.Algebra.Algebra.Pi

Goal state before:
pp: α : Type u_1
β : Type u_2
R : Type u_3
ι : Type u_4
A₁ : ι → Type u_5
A₂ : ι → Type u_6
A₃ : ι → Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → Semiring (A₁ i)
inst✝⁶ : (i : ι) → Semiring (A₂ i)
inst✝⁵ : (i : ι) → Semiring (A₃ i)
inst✝⁴ : (i : ι) → Algebra R (A₁ i)
inst✝³ : (i : ι) → Algebra R (A₂ i)
inst✝² : (i : ι) → Algebra R (A₃ i)
S : Type u_8
inst✝¹ : Semiring S
inst✝ : Algebra R S
⊢ ∀ (x : R),
    (RingEquiv.sumArrowEquivProdArrow α β S) ((algebraMap R (α ⊕ β → S)) x) = (algebraMap R ((α → S) × (β → S))) x

Tactic:
intro; ext <;> simp

Goal state after:
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
⊢ Finsupp.single m 1 ∈ ⇑(coeffLinearEquiv R).toEquiv '' ↑(Submodule.span R ((fun x ↦ single x 1) '' s)) ↔ m ∈ s

Tactic:
change _ ∈ (Submodule.span R _).map (coeffLinearEquiv R).toLinearMap ↔ _

Goal state after:
R : Type u_1
M : Type u_3
inst✝¹ : Semiring R
inst✝ : Nontrivial R
m : M
s : Set M
⊢ Finsupp.single m 1 ∈ Submodule.map (↑(coeffLinearEquiv R)) (Submodule.span R ((fun x ↦ single x 1) '' s)) ↔ m ∈ s
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
hs : Disjoint s t
i : α
⊢ (⨅ a ∈ sᶜ, (lapply a).ker) ⊓ ⨅ a ∈ tᶜ, (lapply a).ker ≤ (lapply i).ker

Tactic:
by_cases his : i ∈ s

Goal state after:
case pos
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
hs : Disjoint s t
i : α
his : i ∈ s
⊢ (⨅ a ∈ sᶜ, (lapply a).ker) ⊓ ⨅ a ∈ tᶜ, (lapply a).ker ≤ (lapply i).ker

case neg
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
hs : Disjoint s t
i : α
his : i ∉ s
⊢ (⨅ a ∈ sᶜ, (lapply a).ker) ⊓ ⨅ a ∈ tᶜ, (lapply a).ker ≤ (lapply i).ker
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
a : α
⊢ {a⁻¹⁻¹} = {a}

Tactic:
inv_inv

Goal state after:
α : Type u_2
inst✝ : Group α
a : α
⊢ {a} = {a}
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
b : α
⊢ {b⁻¹⁻¹} = {b}

Tactic:
inv_inv

Goal state after:
α : Type u_2
inst✝ : Group α
b : α
⊢ {b} = {b}
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq β
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
n : ℕ
x✝ : n + 2 ≠ 0
⊢ ∀ (f : F) (s : Finset α), image (⇑f) (s ^ (n + 2)) = image (⇑f) s ^ (n + 2)

Tactic:
simp [image_mul, pow_succ _ n.succ, image_pow_of_ne_zero]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelMonoid α
s : Finset α
m n : ℕ
hm : m ≠ 0
hmn : m ≤ n
⊢ #(s ^ m) ≤ #(s ^ n)

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Goal state after:
case inl
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelMonoid α
m n : ℕ
hm : m ≠ 0
hmn : m ≤ n
⊢ #(∅ ^ m) ≤ #(∅ ^ n)

case inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelMonoid α
s : Finset α
m n : ℕ
hm : m ≠ 0
hmn : m ≤ n
hs : s.Nonempty
⊢ #(s ^ m) ≤ #(s ^ n)
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R[ℕ]
n : ℕ
⊢ { toFinsupp := a ^ n } = { toFinsupp := a } ^ n

Tactic:
change _ = npowRec n _

Goal state after:
R : Type u
inst✝ : Semiring R
a : R[ℕ]
n : ℕ
⊢ { toFinsupp := a ^ n } = npowRec n { toFinsupp := a }
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : p ∈ f.invtSubmodule
hq : q ∈ f.invtSubmodule
⊢ Disjoint ⟨p, hp⟩ ⟨q, hq⟩ ↔ Disjoint p q

Tactic:
disjoint_iff,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : p ∈ f.invtSubmodule
hq : q ∈ f.invtSubmodule
⊢ ⟨p, hp⟩ ⊓ ⟨q, hq⟩ = ⊥ ↔ Disjoint p q
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : p ∈ f.invtSubmodule
hq : q ∈ f.invtSubmodule
⊢ ⟨p, hp⟩ ⊓ ⟨q, hq⟩ = ⊥ ↔ Disjoint p q

Tactic:
disjoint_iff,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : p ∈ f.invtSubmodule
hq : q ∈ f.invtSubmodule
⊢ ⟨p, hp⟩ ⊓ ⟨q, hq⟩ = ⊥ ↔ p ⊓ q = ⊥
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a b : R
inst✝ : Ring R
n : ℕ
⊢ (monomial n) (a - b) = (monomial n) a - (monomial n) b

Tactic:
rw [sub_eq_add_neg, map_add, monomial_neg, sub_eq_add_neg]

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

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
x✝ : (i : ι) × φ i
i : ι
x : φ i
j : ι
y : φ j
h : i = j
⊢ ((Finsupp.basis b).repr (single ⟨i, x⟩.fst ((b ⟨i, x⟩.fst) ⟨i, x⟩.snd))) ⟨j, y⟩ = (single ⟨i, x⟩ 1) ⟨j, y⟩

pp: case neg
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
x✝ : (i : ι) × φ i
i : ι
x : φ i
j : ι
y : φ j
h : ¬i = j
⊢ ((Finsupp.basis b).repr (single ⟨i, x⟩.fst ((b ⟨i, x⟩.fst) ⟨i, x⟩.snd))) ⟨j, y⟩ = (single ⟨i, x⟩ 1) ⟨j, y⟩

Tactic:
· cases h
        simp [Finsupp.single_apply_left sigma_mk_injective]

Goal state after:
case neg
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
x✝ : (i : ι) × φ i
i : ι
x : φ i
j : ι
y : φ j
h : ¬i = j
⊢ ((Finsupp.basis b).repr (single ⟨i, x⟩.fst ((b ⟨i, x⟩.fst) ⟨i, x⟩.snd))) ⟨j, y⟩ = (single ⟨i, x⟩ 1) ⟨j, y⟩
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
S : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Module S N
inst✝¹ : SMulCommClass R S N
inst✝ : Module.Finite R M
s : Finset M
span_s : Submodule.span R ↑s = ⊤
x : M →ₗ[R] ι →₀ N
⊢ (finsuppLinearMap S) (onFinset (s.sup fun m ↦ (x m).support) (fun x_1 ↦ lapply x_1 ∘ₗ x) ⋯) = x

Tactic:
· ext; rfl

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

Goal state before:
pp: ι : Sort u_1
f : ι → ℕ∞
n : ℕ
⊢ ⨅ i, f i = ↑n ↔ (∃ i, f i = ↑n) ∧ ∀ (i : ι), ↑n ≤ f i

Tactic:
by
  by_cases! hι : IsEmpty ι
  · simp [iInf_of_isEmpty]
  apply ciInf_eq_iff

Goal state after:
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
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : { f // IsIdempotentElem f ∧ range f = p }
x : E
⊢ ↑f x ∈ p

Tactic:
simp_rw [← f.2.2]; exact mem_range_self f.1 x

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
⊢ IsProj f.range f ↔ IsIdempotentElem f

Tactic:
by
  refine ⟨fun ⟨h1, h2⟩ => ?_, fun hf =>
    ⟨fun x => mem_range_self f x, fun x ⟨y, hy⟩ => by rw [← hy, ← Module.End.mul_apply, hf.eq]⟩⟩
  ext x
  exact h2 (f x) (h1 x)

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
y : RelSeries r
nx : ℕ
fx : Fin (nx + 1) → α
step✝ : ∀ (i : Fin nx), (fx i.castSucc, fx i.succ) ∈ r
length_eq : nx = y.length
toFun_eq : { length := nx, toFun := fx, step := step✝ }.toFun = y.toFun ∘ Fin.cast ⋯
⊢ { length := nx, toFun := fx, step := step✝ } = y

Tactic:
subst length_eq

Goal state after:
α : Type u_1
r : SetRel α α
y : RelSeries r
fx : Fin (y.length + 1) → α
step✝ : ∀ (i : Fin y.length), (fx i.castSucc, fx i.succ) ∈ r
toFun_eq : { length := y.length, toFun := fx, step := step✝ }.toFun = y.toFun ∘ Fin.cast ⋯
⊢ { length := y.length, toFun := fx, step := step✝ } = y
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}
this : (↑x).length.pred.succ = (↑x).length
⊢ (↑((fun x ↦ ⟨x.toList, ⋯⟩) ((fun x ↦ fromListIsChain ↑x ⋯ ⋯) x))).length = (↑x).length

Tactic:
simp_all [toList]

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

Goal state before:
pp: case a.mem.zero
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
a : M
ha : a ∈ s
⊢ (f a) 0 ∈ span R (image2 (fun m n ↦ (f m) n) s t)

Tactic:
intros

Goal state after:
case a.mem.zero
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
a : M
ha : a ∈ s
⊢ (f a) 0 ∈ span R (image2 (fun m n ↦ (f m) n) s t)
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: case a.mem.add
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
a : M
ha : a ∈ s
⊢ ∀ (x y : N),
    x ∈ span R t →
      y ∈ span R t →
        (f a) x ∈ span R (image2 (fun m n ↦ (f m) n) s t) →
          (f a) y ∈ span R (image2 (fun m n ↦ (f m) n) s t) → (f a) (x + y) ∈ span R (image2 (fun m n ↦ (f m) n) s t)

Tactic:
intros

Goal state after:
case a.mem.add
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
a : M
ha : a ∈ s
x✝ y✝ : N
hx✝ : x✝ ∈ span R t
hy✝ : y✝ ∈ span R t
a✝¹ : (f a) x✝ ∈ span R (image2 (fun m n ↦ (f m) n) s t)
a✝ : (f a) y✝ ∈ span R (image2 (fun m n ↦ (f m) n) s t)
⊢ (f a) (x✝ + y✝) ∈ span R (image2 (fun m n ↦ (f m) n) s t)
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: case a.mem.smul
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
a : M
ha : a ∈ s
⊢ ∀ (a_1 : R),
    ∀ x ∈ span R t,
      (f a) x ∈ span R (image2 (fun m n ↦ (f m) n) s t) → (f a) (a_1 • x) ∈ span R (image2 (fun m n ↦ (f m) n) s t)

Tactic:
intros

Goal state after:
case a.mem.smul
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
a : M
ha : a ∈ s
a✝¹ : R
x✝ : N
hx✝ : x✝ ∈ span R t
a✝ : (f a) x✝ ∈ span R (image2 (fun m n ↦ (f m) n) s t)
⊢ (f a) (a✝¹ • x✝) ∈ span R (image2 (fun m n ↦ (f m) n) s t)
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: case a.zero
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
⊢ ∀ n ∈ span R t, (f 0) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)

Tactic:
intros

Goal state after:
case a.zero
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
n✝ : N
a✝ : n✝ ∈ span R t
⊢ (f 0) n✝ ∈ span R (image2 (fun m n ↦ (f m) n) s t)
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: case a.add
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 y : M),
    x ∈ span R s →
      y ∈ span R s →
        (∀ n ∈ span R t, (f x) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)) →
          (∀ n ∈ span R t, (f y) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)) →
            ∀ n ∈ span R t, (f (x + y)) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)

Tactic:
intros

Goal state after:
case a.add
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✝ y✝ : M
hx✝ : x✝ ∈ span R s
hy✝ : y✝ ∈ span R s
a✝² : ∀ n ∈ span R t, (f x✝) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)
a✝¹ : ∀ n ∈ span R t, (f y✝) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)
n✝ : N
a✝ : n✝ ∈ span R t
⊢ (f (x✝ + y✝)) n✝ ∈ span R (image2 (fun m n ↦ (f m) n) s t)
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: case a.smul
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
⊢ ∀ (a : R),
    ∀ x ∈ span R s,
      (∀ n ∈ span R t, (f x) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)) →
        ∀ n ∈ span R t, (f (a • x)) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)

Tactic:
intros

Goal state after:
case a.smul
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
a✝² : R
x✝ : M
hx✝ : x✝ ∈ span R s
a✝¹ : ∀ n ∈ span R t, (f x✝) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)
n✝ : N
a✝ : n✝ ∈ span R t
⊢ (f (a✝² • x✝)) n✝ ∈ span R (image2 (fun m n ↦ (f m) n) s t)
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
h : ∀ (a : α), ∀ b < f a, ∃ a' < a, f a' = b
a : α
⊢ height a = height (f a)

Tactic:
have : coheight (OrderDual.toDual a) = coheight (OrderDual.toDual (f a)) :=
    coheight_eq_of_strictMono (α := αᵒᵈ) (β := βᵒᵈ) (f := OrderDual.toDual ∘ f ∘ OrderDual.toDual)
    (strictMono_dual_iff.mp hf) (fun a b hab ↦ h a b hab) _

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
h : ∀ (a : α), ∀ b < f a, ∃ a' < a, f a' = b
a : α
this : coheight (OrderDual.toDual a) = coheight (OrderDual.toDual (f a))
⊢ height a = height (f a)
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝³⁶ : CommSemiring R
inst✝³⁵ : CommSemiring R₂
inst✝³⁴ : CommSemiring R₃
inst✝³³ : Monoid R'
inst✝³² : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝³¹ : AddCommMonoid M
inst✝³⁰ : AddCommMonoid N
inst✝²⁹ : AddCommMonoid P
inst✝²⁸ : AddCommMonoid Q
inst✝²⁷ : AddCommMonoid S
inst✝²⁶ : AddCommMonoid P'
inst✝²⁵ : AddCommMonoid Q'
inst✝²⁴ : AddCommMonoid M₂
inst✝²³ : AddCommMonoid N₂
inst✝²² : AddCommMonoid P₂
inst✝²¹ : AddCommMonoid Q₂
inst✝²⁰ : AddCommMonoid M₃
inst✝¹⁹ : AddCommMonoid N₃
inst✝¹⁸ : AddCommMonoid P₃
inst✝¹⁷ : AddCommMonoid Q₃
inst✝¹⁶ : DistribMulAction R' M
inst✝¹⁵ : Module R'' M
inst✝¹⁴ : Module R M
inst✝¹³ : Module R N
inst✝¹² : Module R S
inst✝¹¹ : Module R P'
inst✝¹⁰ : Module R Q'
inst✝⁹ : Module R₂ M₂
inst✝⁸ : Module R₂ N₂
inst✝⁷ : Module R₂ P₂
inst✝⁶ : Module R₂ Q₂
inst✝⁵ : Module R₃ M₃
inst✝⁴ : Module R₃ N₃
inst✝³ : Module R₃ P₃
inst✝² : Module R₃ Q₃
inst✝¹ : SMulCommClass R R' M
inst✝ : SMulCommClass R R'' M
r : R'
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
s : R
m : M
n : N
⊢ (s • r • m) ⊗ₜ[R] n = (r • m) ⊗ₜ[R] (s • n)

Tactic:
smul_tmul

Goal state after:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝³⁶ : CommSemiring R
inst✝³⁵ : CommSemiring R₂
inst✝³⁴ : CommSemiring R₃
inst✝³³ : Monoid R'
inst✝³² : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝³¹ : AddCommMonoid M
inst✝³⁰ : AddCommMonoid N
inst✝²⁹ : AddCommMonoid P
inst✝²⁸ : AddCommMonoid Q
inst✝²⁷ : AddCommMonoid S
inst✝²⁶ : AddCommMonoid P'
inst✝²⁵ : AddCommMonoid Q'
inst✝²⁴ : AddCommMonoid M₂
inst✝²³ : AddCommMonoid N₂
inst✝²² : AddCommMonoid P₂
inst✝²¹ : AddCommMonoid Q₂
inst✝²⁰ : AddCommMonoid M₃
inst✝¹⁹ : AddCommMonoid N₃
inst✝¹⁸ : AddCommMonoid P₃
inst✝¹⁷ : AddCommMonoid Q₃
inst✝¹⁶ : DistribMulAction R' M
inst✝¹⁵ : Module R'' M
inst✝¹⁴ : Module R M
inst✝¹³ : Module R N
inst✝¹² : Module R S
inst✝¹¹ : Module R P'
inst✝¹⁰ : Module R Q'
inst✝⁹ : Module R₂ M₂
inst✝⁸ : Module R₂ N₂
inst✝⁷ : Module R₂ P₂
inst✝⁶ : Module R₂ Q₂
inst✝⁵ : Module R₃ M₃
inst✝⁴ : Module R₃ N₃
inst✝³ : Module R₃ P₃
inst✝² : Module R₃ Q₃
inst✝¹ : SMulCommClass R R' M
inst✝ : SMulCommClass R R'' M
r : R'
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
s : R
m : M
n : N
⊢ (r • m) ⊗ₜ[R] (s • n) = (r • m) ⊗ₜ[R] (s • n)
Module: Mathlib.Algebra.Algebra.Bilinear

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
⊢ IsUnit x ↔ Function.Bijective ⇑((Algebra.lmul R A) x)

Tactic:
exact IsUnit.isUnit_iff_mulLeft_bijective

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : Fintype ι
f : ι → Set α
a : α
⊢ a ∈ ∏ i, f i ↔ ∃ g, ∃ (_ : ∀ (i : ι), g i ∈ f i), ∏ i, g i = a

Tactic:
by
  rw [mem_finsetProd]
  simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝¹ : M
x✝ : N
⊢ (((mk R M N).compr₂ₛₗ (map LinearMap.id LinearMap.id)) x✝¹) x✝ = (((mk R M N).compr₂ₛₗ LinearMap.id) x✝¹) x✝

Tactic:
simp only [mk_apply, id_coe, compr₂ₛₗ_apply, _root_.id, map_tmul]

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: case base
α : Type u_1
inst✝ : IdemSemiring α
n : ℕ
⊢ ↑1 = 1

Tactic:
exact Nat.cast_one

Goal state after:
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : R
⊢ 0 * x + 1 * 1 = 1

Tactic:
rw [one_mul, zero_mul, zero_add]

Goal state after:
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semifield R
m n : R
⊢ IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0

Tactic:
obtain rfl | hn := eq_or_ne n 0

Goal state after:
case inl
R : Type u_1
inst✝ : Semifield R
m : R
⊢ IsCoprime m 0 ↔ m ≠ 0 ∨ 0 ≠ 0

case inr
R : Type u_1
inst✝ : Semifield R
m n : R
hn : n ≠ 0
⊢ IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: case neg
α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := List.ofFn val
sli : List α := li.mergeSort fun a b ↦ decide (a ≤ b)
this : ∀ (i : Fin n), ∃ j, sli[j] = val i
i j : Fin n
h_eq : ¬val i = val j
pf✝ : ∀ (j : Fin sli.length), ↑j < sli.length
hi : ∃ j, sli[↑j] = val i
hj : ∃ j_1, sli[↑j_1] = val j
⊢ val i ≤ val j ↔ ↑hi.choose ≤ ↑hj.choose

Tactic:
rw [← hi.choose_spec, ← hj.choose_spec] at h_eq

Goal state after:
case neg
α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := List.ofFn val
sli : List α := li.mergeSort fun a b ↦ decide (a ≤ b)
this : ∀ (i : Fin n), ∃ j, sli[j] = val i
i j : Fin n
pf✝ : ∀ (j : Fin sli.length), ↑j < sli.length
hi : ∃ j, sli[↑j] = val i
hj : ∃ j_1, sli[↑j_1] = val j
h_eq : ¬sli[↑hi.choose] = sli[↑hj.choose]
⊢ val i ≤ val j ↔ ↑hi.choose ≤ ↑hj.choose
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mem_mul : ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C i.succ (m * x) ⋯
n : ℕ
x : A
hx : x ∈ M ^ n
⊢ C n x hx

Tactic:
induction n generalizing x with

Goal state after: