mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case zero
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
⊢ 0 < c.ord → derivFamily f 0 < c.ord

Tactic:
rw [derivFamily_zero]
    exact nfpFamily_lt_ord_lift hω (by rwa [hc.cof_ord]) hf

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
p : ι → Prop
inst✝ : DecidablePred p
⊢ filter p 0 = 0

Tactic:
by
  ext
  simp

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
⊢ f.update i (f i) = f

Tactic:
by
  ext
  simp

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
C : ((i : ι) → Quotient (S i)) → Sort u_4
a : (i : ι) → α i
⊢ (finHRecOn fun x ↦ ⟦a x⟧) = fun f x ↦ f a

Tactic:
by
  ext f h
  refine eq_of_heq ((eqRec_heq _ _).trans ?_)
  rw [finChoice_eq]
  rfl

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : ι →₀ M
⊢ f.toDFinsupp.support = f.support

Tactic:
by
  ext
  simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : Π₀ (x : ι), M
⊢ f.toFinsupp.support = f.support

Tactic:
by
  ext
  simp

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : Π₀ (i : ι), β i
⊢ (erase i f).support = f.support.erase i

Tactic:
by
  ext
  simp

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
⊢ (subtypeDomain p f).support = Finset.subtype p f.support

Tactic:
by
  ext
  simp

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

Goal state before:
pp: ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
f g : Π₀ (i : ι), β i
⊢ comapDomain' h hh' (f + g) = comapDomain' h hh' f + comapDomain' h hh' g

Tactic:
ext
  rw [add_apply, comapDomain'_apply, comapDomain'_apply, comapDomain'_apply, add_apply]

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

Goal state before:
pp: ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
f : (i : ι) → β₁ i →+ β₂ i
f₂ : (i : ι) → β i →+ β₁ i
⊢ (addMonoidHom fun i ↦ (f i).comp (f₂ i)) = (addMonoidHom f).comp (addMonoidHom f₂)

Tactic:
by
  ext
  simp

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

Goal state before:
pp: ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
f : (i : ι) → β i ≃+ β₁ i
f₂ : (i : ι) → β₁ i ≃+ β₂ i
⊢ (addEquiv fun i ↦ (f i).trans (f₂ i)) = (addEquiv f).trans (addEquiv f₂)

Tactic:
by
  ext
  simp

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring S
inst✝⁸ : Semiring S₂
M : Type u_5
N : Type u_7
P : Type u_9
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M
inst✝³ : Module S N
inst✝² : Module R₂ P
inst✝¹ : Module S₂ P
inst✝ : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
H : f.flip = g.flip
m : M
n : N
⊢ (f.flip n) m = (g.flip n) m

Tactic:
rw [H]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : (m : R) → Decidable (m ≠ 0)
p : ι → Submodule R N
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
⊢ ((lsum ℕ) fun i ↦ (p i).subtype) ∘ₗ
      (mapRange.linearMap fun i ↦ LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) ∘ₗ ↑(finsuppLequivDFinsupp R) =
    Finsupp.linearCombination R v

Tactic:
by
  ext
  simp

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x → x = 0
m : Π₀ (i : ι), ↥(p i)
hm : ((lsum ℕ) fun i ↦ (p i).subtype) m = 0
i : ι
⊢ m i = 0

Tactic:
← neg_eq_zero

Goal state after:
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x → x = 0
m : Π₀ (i : ι), ↥(p i)
hm : ((lsum ℕ) fun i ↦ (p i).subtype) m = 0
i : ι
⊢ -m i = 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
⊢ (∀ (s t : R), s • -x + t • y = 0 → s = 0 ∧ t = 0) ↔ ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0

Tactic:
refine ⟨fun h s t hst ↦ ?_, fun h s t hst ↦ ?_⟩ <;> simpa using h (-s) t (by simpa using hst)

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
S T : Submodule R M
hST : T ≤ S
⊢ Nat.card ↥(map T.mkQ S) * Nat.card (M ⧸ S) = Nat.card (M ⧸ T)

Tactic:
by
  rw [Submodule.card_eq_card_quotient_mul_card (map T.mkQ S),
    Nat.card_congr (quotientQuotientEquivQuotient T S hST).toEquiv]

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

Goal state before:
pp: case neg
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
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
hbd : ¬(b = 0 ∧ d = 0)
⊢ ∃ s t, s • (a • x + b • y) + t • (c • x + d • y) = 0 ∧ (s = 0 → t ≠ 0)

Tactic:
refine ⟨d • 1, -b • 1, ?_, by contrapose! hbd; simp_all⟩

Goal state after:
case neg
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
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
hbd : ¬(b = 0 ∧ d = 0)
⊢ (d • 1) • (a • x + b • y) + (-b • 1) • (c • x + d • y) = 0
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
⊢ toFinsupp.comp toFreeAbelianGroup = AddMonoidHom.id (X →₀ ℤ)

Tactic:
by
  ext
  simp

Goal state after:
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
f : ι → Dual R M
h1 : Pairwise fun i j ↦ (f i) (v j) = 0
h2 : ∀ (i : ι), (f i) (v i) = 1
⊢ LinearIndependent R v

Tactic:
refine linearIndependent_iff'.mpr fun s g hrel i hi ↦ ?_
  have aux (j : ι) (hjs : j ∈ s) (hji : j ≠ i) : g j * (f i) (v j) = 0 := by simp [h1 hji.symm]
  simpa [s.sum_eq_single i aux (by lia), h2 i] using congr_arg (f i) hrel

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

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

Tactic:
obtain ⟨r, hr, l, hl, hg⟩ := hg

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

Goal state before:
pp: ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
x✝¹ x✝ : A
⊢ { toFun := fun ψ ↦ ψ (x✝¹ + x✝), map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ } =
    { toFun := fun ψ ↦ ψ x✝¹, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ } +
      { toFun := fun ψ ↦ ψ x✝, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ }

Tactic:
by ext; simp [map_add_eq_mul]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
n : ℕ
x : R
⊢ ψ x ^ n = (ψ.mulShift ↑n) x

Tactic:
← mulShift_spec'

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
n : ℕ
x : R
⊢ (ψ.mulShift ↑n) x = (ψ.mulShift ↑n) x
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f f' : α → β → γ
s : Finset α
t : Finset β
h : ∀ a ∈ s, ∀ b ∈ t, f a b = f' a b
⊢ image2 f ↑s ↑t = image2 f' ↑s ↑t

Tactic:
exact image2_congr h

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

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst✝³ : DecidableEq α'
inst✝² : DecidableEq β'
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
⊢ image g (image₂ f s t) = image₂ f' (image g₁ t) (image g₂ s)

Tactic:
rw [image₂_swap f]
  exact image_image₂_distrib fun _ _ => h_antidistrib _ _

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

Goal state before:
pp: case pos
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : M × M → R := fun p ↦ if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0
p : M × M
hps : p ∈ s
hp : p ∈ s → x.coeff p.1 ≠ 0 → y.coeff p.2 = 0
h1 : x.coeff p.1 = 0
⊢ x.coeff p.1 * y.coeff p.2 = 0

Tactic:
rw [h1, zero_mul]

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

Goal state before:
pp: α : Type u_1
s : Finset α
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : Std.Antisymm r
inst✝ : Std.Total r
⊢ s.val.Nodup

Tactic:
exact s.2

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : InvolutiveInv α
s : Finset α
⊢ ↑(s.preimage (fun x ↦ x⁻¹) ⋯) = ↑s⁻¹

Tactic:
coe_preimage,

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : InvolutiveInv α
s : Finset α
⊢ (fun x ↦ x⁻¹) ⁻¹' ↑s = ↑s⁻¹
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 * a * (b * a2) = b1 * a1 * (b2 * a2)

Tactic:
mul_assoc b1,

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 * (a * (b * a2)) = b1 * a1 * (b2 * a2)
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝³ : Semiring R
p q : R[X]
S : Type u_1
inst✝² : Semiring S
inst✝¹ : Module S R
inst✝ : IsTorsionFree S R
s : S
hs : IsRegular s
⊢ IsSMulRegular R[X] s

Tactic:
rintro ⟨f⟩ ⟨g⟩ hfg; congr; apply hs.isSMulRegular; simpa using congr(($hfg).toFinsupp)

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

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q : R[X]
inst✝ : Subsingleton R
⊢ ∀ (a : R[X]), a = default

Tactic:
by
      rintro ⟨x⟩
      apply congr_arg ofFinsupp
      simp [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: R : Type u
inst✝ : DivisionRing R
a : ℚ
f : R[X]
⊢ a • f = C ↑a * f

Tactic:
← Rat.smul_one_eq_cast,

Goal state after:
R : Type u
inst✝ : DivisionRing R
a : ℚ
f : R[X]
⊢ a • f = C (a • 1) * f
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : DivisionRing R
a : ℚ
f : R[X]
⊢ a • f = C ↑a * f

Tactic:
rw [← Rat.smul_one_eq_cast, ← Polynomial.smul_C, C_1, smul_one_mul]

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
⊢ Codisjoint p f.ker

Tactic:
rw [codisjoint_iff_le_sup]
    intro x _
    rw [mem_sup']
    refine ⟨f x, ⟨x - f x, ?_⟩, add_sub_cancel _ _⟩
    rw [mem_ker, map_sub, hf, sub_self]

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
p q : Submodule R E
hpq : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
⊢ (ofIsCompl hpq φ ψ).range = φ.range ⊔ ψ.range

Tactic:
by
  rw [ofIsCompl_eq_add]
  apply le_antisymm
  · apply range_add_le _ _ |>.trans
    gcongr
    all_goals exact range_comp_le_range ..
  · apply sup_le
    all_goals rintro - ⟨x, rfl⟩; exact ⟨x, by simp⟩

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

Goal state before:
pp: ι : Sort u_1
f : ι → ℕ∞
⊢ ⨅ i, f i = 0 ↔ ∃ i, f i = 0

Tactic:
by
  simpa [Order.lt_one_iff] using iInf_lt_iff (α := ℕ∞) (a := 1)

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

Goal state before:
pp: case inr.inr.coe
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
hne : a ≠ 0
hι : Nonempty ι
d : ℕ
h : ∀ (i : ι), a * f i ≤ ↑d
hlt : ⨆ i, f i < ⊤
j : ι
hj : f j = ⨆ i, f i
⊢ a * ⨆ i, f i ≤ ↑d

Tactic:
rw [← hj]

Goal state after:
case inr.inr.coe
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
hne : a ≠ 0
hι : Nonempty ι
d : ℕ
h : ∀ (i : ι), a * f i ≤ ↑d
hlt : ⨆ i, f i < ⊤
j : ι
hj : f j = ⨆ i, f i
⊢ a * f j ≤ ↑d
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
⊢ Exact ⇑(LinearMap.inl R M N) ⇑(LinearMap.snd R M N)

Tactic:
rintro ⟨x, y⟩
  simp only [LinearMap.snd_apply, @eq_comm _ y, LinearMap.coe_inl, Set.mem_range, Prod.mk.injEq,
    exists_eq_left]

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

Goal state before:
pp: ι : Sort uι
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 : ι → Submodule R M
t : Submodule R N
⊢ map₂ f (⨆ i, s i) t = ⨆ i, map₂ f (s i) t

Tactic:
suffices map₂ f (⨆ i, span R (s i : Set M)) (span R t) = ⨆ i, map₂ f (span R (s i)) (span R t) by
    simpa only [span_eq] using this
  simp_rw [map₂_span_span, ← span_iUnion, map₂_span_span, Set.image2_iUnion_left]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
x : α
inst✝ : OrderTop α
h : x < ⊤
⊢ 0 < coheight x

Tactic:
rw [coheight_pos]

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
x : α
inst✝ : OrderTop α
h : x < ⊤
⊢ ¬IsMax x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfiniteDimensionalOrder α
m✝ : WithBot ℕ∞
hm✝ : ∀ (i : LTSeries α), ↑i.length ≤ m✝
m : WithBot ℕ∞
hm : ∀ (i : LTSeries α), ↑i.length ≤ m
⊢ ⊤ ≤ m

Tactic:
rw [top_le_iff, ENat.WithBot.eq_top_iff_forall_ge]

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfiniteDimensionalOrder α
m✝ : WithBot ℕ∞
hm✝ : ∀ (i : LTSeries α), ↑i.length ≤ m✝
m : WithBot ℕ∞
hm : ∀ (i : LTSeries α), ↑i.length ≤ m
⊢ ∀ (m_1 : ℕ), ↑m_1 ≤ m
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝ : IsEmpty α
⊢ ↑n ≤ krullDim α ↔ ∃ l, l.length = n

Tactic:
simp [krullDim_eq_bot]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : A
n : ℕ
⊢ mulRight R a ^ 0 = mulRight R (a ^ 0)

Tactic:
by rw [pow_zero, pow_zero, mulRight_one, Module.End.one_eq_id]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
⊢ IsCoprime x y ∧ IsCoprime z x ↔ IsCoprime x y ∧ IsCoprime x z

Tactic:
@isCoprime_comm _ _ z

Goal state after:
R : Type u
inst✝ : CommSemiring R
x y z : R
⊢ IsCoprime x y ∧ IsCoprime x z ↔ IsCoprime x y ∧ IsCoprime x z
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x y z : R
⊢ IsCoprime (x - y * z) y ↔ IsCoprime x y

Tactic:
by
  rw [sub_eq_add_neg, ← mul_neg, add_mul_left_left_iff]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y z : R
⊢ IsRelPrime (x - y * z) y ↔ IsRelPrime x y

Tactic:
by
  rw [sub_eq_add_neg, ← mul_neg, add_mul_left_left_iff]

Goal state after:
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: case h
α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := ⋯
sli : List α := ⋯
this : ∀ (i : Fin n), ∃ j, sli[j] = val i
⊢ ∀ (i j : Fin n), val i ≤ val j ↔ (fun i ↦ ↑↑⋯.choose) i ≤ (fun i ↦ ↑↑⋯.choose) j

Tactic:
intro i j

Goal state after:
case h
α : 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
⊢ val i ≤ val j ↔ (fun i ↦ ↑↑⋯.choose) i ≤ (fun i ↦ ↑↑⋯.choose) j
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case cons.mp.refine_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ✝ : μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
hμ :
  ∑ x ∈ t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x +
        μ x * ∏ j ∈ insert a t \ {x}, s j) =
    1
⊢ ∑ i ∈ t, (Pi.single (Exists.choose h) (μ a * s (Exists.choose h)) + μ * fun x ↦ s a) i * ∏ j ∈ t \ {i}, s j = 1

Tactic:
rw [← hμ, sum_congr rfl]

Goal state after:
case cons.mp.refine_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ✝ : μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
hμ :
  ∑ x ∈ t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x +
        μ x * ∏ j ∈ insert a t \ {x}, s j) =
    1
⊢ ∀ x ∈ t,
    (Pi.single (Exists.choose h) (μ a * s (Exists.choose h)) + μ * fun x ↦ s a) x * ∏ j ∈ t \ {x}, s j =
      Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x +
        μ x * ∏ j ∈ insert a t \ {x}, s j
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
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
⊢ map f.toLinearMap 1 = 1

Tactic:
by
  ext
  simp

Goal state after:
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
⊢ comap (↑(opLinearEquiv R)) 1 = 1

Tactic:
by
  ext
  simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
x : R
⊢ x ∈ map (RingHom.fst R S) (I.prod J) ↔ x ∈ I

Tactic:
rw [mem_map_iff_of_surjective (RingHom.fst R S) Prod.fst_surjective]

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
x : R
⊢ (∃ x_1 ∈ I.prod J, (RingHom.fst R S) x_1 = x) ↔ x ∈ I
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
⊢ I * (1 / I) ≤ 1

Tactic:
rw [Submodule.mul_le]

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
⊢ ∀ m ∈ I, ∀ n ∈ 1 / I, m * n ∈ 1
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
I✝ J : Ideal R
K L : Ideal S
inst✝ : RingHomClass F R S
I : Ideal S
x y : R
hx : x ∈ ⇑f ⁻¹' ↑I
hy : y ∈ ⇑f ⁻¹' ↑I
⊢ x + y ∈ ⇑f ⁻¹' ↑I

Tactic:
by
    simp only [Set.mem_preimage, SetLike.mem_coe, map_add f] at hx hy ⊢
    exact add_mem hx hy

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a b : R
hb : b ≠ 0
h : ¬a - a * b / b = 0
this : ¬a * b % b ≺ b
⊢ False

Tactic:
exact this (mod_lt _ hb)

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
x : ↥N
this : map N.subtype (I • ⊤) = I • N
⊢ x ∈ I • ⊤ ↔ ↑x ∈ I • N

Tactic:
simp [← this, -map_smul'']

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : EuclideanDomain R
b : R
n : ℕ
c : R
hb : b ≠ 0
⊢ (b * c / b) ^ n = (b * c) ^ n / b ^ n

Tactic:
simp [hb, mul_pow]

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
this : x * y ∣ z * gcd x y
⊢ x * y / gcd x y ∣ z

Tactic:
obtain ⟨p, hp⟩ := this

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
p : R
hp : z * gcd x y = x * y * p
⊢ x * y / gcd x y ∣ z
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : EuclideanDomain R
inst✝ : CommRing S
e : S ≃+* R
a b : S
hb : b ≠ 0
⊢ EuclideanDomain.r (e (e.symm (e a % e b))) (e b)

Tactic:
by
    have hb' : e b ≠ 0 := by simpa using hb
    simpa using! EuclideanDomain.remainder_lt (e a) hb'

Goal state after: