mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: case pos
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
x : α
this : DecidablePred fun x ↦ x ∈ s
xs : x ∈ s
⊢ l x = 0 x

Tactic:
have : Finsupp.sum l (fun a => Finsupp.single (f a)) (f x) = 0 := by
      rw [h₂]
      rfl

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
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
x : α
this✝ : DecidablePred fun x ↦ x ∈ s
xs : x ∈ s
this : (l.sum fun a ↦ single (f a)) (f x) = 0
⊢ l x = 0 x
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
⊢ PLift.down ⁻¹' mulSupport f = ⇑Equiv.plift.symm '' mulSupport f

Tactic:
exact (Equiv.plift.symm.image_eq_preimage_symm _).symm

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

Goal state before:
pp: n : ℕ
s : Finset ℕ
h : ∀ m ∈ s, m < n
⊢ map Fin.valEmbedding (s.attachFin h) = s

Tactic:
by
  simp [map_eq_image]

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

Goal state before:
pp: α : Type u_1
R : Type u_5
inst✝² : Semiring R
α' : Type u_7
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
v' : α' → M'
f : α ≃ α'
l : α →₀ R
⊢ (linearCombination R v') (equivMapDomain f l) = (linearCombination R (v' ∘ ⇑f)) l

Tactic:
equivMapDomain_eq_mapDomain,

Goal state after:
α : Type u_1
R : Type u_5
inst✝² : Semiring R
α' : Type u_7
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
v' : α' → M'
f : α ≃ α'
l : α →₀ R
⊢ (linearCombination R v') (mapDomain (⇑f) l) = (linearCombination R (v' ∘ ⇑f)) l
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: case mpr
m n : ℕ
i : Fin (m + n)
⊢ i ∈ {i | m ≤ ↑i} → i ∈ range (natAdd m)

Tactic:
refine fun (hi : m ≤ i) ↦ ⟨⟨i - m, by lia⟩, ?_⟩
    ext
    simp [hi]

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

Goal state before:
pp: case neg
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
c : α
this : DecidablePred fun x ↦ x ∈ s
h : c ∉ s
⊢ z c • v c ∈ span R (v '' s)

Tactic:
· simp [(Finsupp.mem_supported' R _).1 hz _ h]

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

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝ : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst✝⁹ : Semiring R✝
inst✝⁸ : AddCommMonoid M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : Module R✝ M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
R' : Type u_13
inst✝¹ : Semiring R'
inst✝ : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), f c • x = c • x
⊢ Basis ι R' M

Tactic:
letI : Module R' R := Module.compHom R (↑f.symm : R' →+* R)

Goal state after:
ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝ : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst✝⁹ : Semiring R✝
inst✝⁸ : AddCommMonoid M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : Module R✝ M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
R' : Type u_13
inst✝¹ : Semiring R'
inst✝ : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), f c • x = c • x
this : Module R' R := compHom R ↑f.symm
⊢ Basis ι R' M
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case inl
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
x : α
hx : x ∈ mulSupport f
h : x ∉ s → f x = 1
⊢ x ∈ s

pp: case inr
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
s : Set α
h : a ∉ s → f a = 1
x : α
hx : x ∈ mulSupport f
hxs : x ∈ s
⊢ x ∈ s

Tactic:
exacts [not_imp_comm.1 h hx, hxs]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
inst✝ : NeZero m
i : Fin n
⊢ map (castAddEmb m) (Ici i) = Ico (castAdd m i) (natAdd n 0)

Tactic:
by
  simp [map_eq_image]

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin n
hi : i ≠ 0
⊢ ↑((Equiv.symm (finRotate n)) i) = ↑i - 1

Tactic:
by
  rwa [finRotate_symm_apply, Fin.val_sub_one_of_ne_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
p : Submodule R M
⊢ p = ⊤ ↔ ∀ (i : ι), b i ∈ p

Tactic:
refine ⟨fun h ↦ by simp [h], fun h ↦ ?_⟩
  replace h : range b ⊆ p := by rintro - ⟨i, rfl⟩; exact h i
  simpa using span_mono (R := R) h

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b c d p : M
hab : ∃ m n, m • p + a = n • p + b
hcd : ∃ m n, m • p + c = n • p + d
⊢ ∃ m n, m • p + (a + c) = n • p + (b + d)

Tactic:
rcases hab with ⟨k, l, hab⟩

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
a b c d p : M
hcd : ∃ m n, m • p + c = n • p + d
k l : ℕ
hab : k • p + a = l • p + b
⊢ ∃ m n, m • p + (a + c) = n • p + (b + d)
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: case h
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
m : ℤ
h : m • p = b - a
⊢ ↑m.toNat • p - ↑(-m).toNat • p = b - a

Tactic:
sub_eq_add_neg,

Goal state after:
case h
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
m : ℤ
h : m • p = b - a
⊢ ↑m.toNat • p + -(↑(-m).toNat • p) = b - a
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a b d : ℕ
hac : a.Coprime (d * b)
b_dvd_c : b ∣ d * b
⊢ a.gcd d * b = b

Tactic:
convert! one_mul b

Goal state after:
a b d : ℕ
hac : a.Coprime (d * b)
b_dvd_c : b ∣ d * b
⊢ a.gcd d = 1
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a : ℕ
⊢ a ≡ 0 [MOD n] ↔ n ∣ a

Tactic:
rw [ModEq, zero_mod, dvd_iff_mod_eq_zero]

Goal state after:
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m n a b : ℕ
h : a ≡ b [MOD n.gcd m]
hn : n ≠ 0
hm : m ≠ 0
⊢ ↑(chineseRemainder' h) < n.lcm m

Tactic:
by
  dsimp only [chineseRemainder']
  rw [dif_neg hn, dif_neg hm, Subtype.coe_mk, xgcd_val, ← Int.toNat_natCast (lcm n m)]
  have lcm_pos := Int.natCast_pos.mpr (Nat.pos_of_ne_zero (lcm_ne_zero hn hm))
  exact (Int.toNat_lt_toNat lcm_pos).mpr (Int.emod_lt_of_pos _ lcm_pos)

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_3
| 1 < #α

Tactic:
rw [← Nat.cast_one]

Goal state after:
α : Type u_3
| ↑1 < #α
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: case a
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝ : Infinite α
b_1 : card β = 1
⊢ 1 ≤ card (α → β)

Tactic:
let := (one_le_card_iff_nonempty β).1 b_1.ge
        exact (one_le_card_iff_nonempty (α → β)).2 Pi.instNonempty

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

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : LinearOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : AddRightReflectLE R
inst✝² : IsCancelAdd M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
h : ∀ (t : Finset ι) (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : ∑ i ∈ t₁, f i • v i = ∑ i ∈ t₂, f i • v i
⊢ ∑ i ∈ t₁, (if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) • v i = ∑ x ∈ t₂, (if x ∈ t₁ ∨ x ∈ t₂ then f x else 0) • v x

pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : LinearOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : AddRightReflectLE R
inst✝² : IsCancelAdd M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
h : ∀ (t : Finset ι) (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : ∑ i ∈ t₁, f i • v i = ∑ i ∈ t₂, f i • v i
⊢ ∀ x ∈ t₁ᶜ, x ∉ t₂ → (if x ∈ t₁ ∨ x ∈ t₂ then f x else 0) • v x = 0

Tactic:
· convert! heq using 2 with i hi i hi <;> simp [hi]

Goal state after:
case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : LinearOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : AddRightReflectLE R
inst✝² : IsCancelAdd M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
h : ∀ (t : Finset ι) (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : ∑ i ∈ t₁, f i • v i = ∑ i ∈ t₂, f i • v i
⊢ ∀ x ∈ t₁ᶜ, x ∉ t₂ → (if x ∈ t₁ ∨ x ∈ t₂ then f x else 0) • v x = 0
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type w
S : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring S
inst✝³ : Algebra R S
R' : Type w'
S' : Type v'
inst✝² : CommSemiring R'
inst✝¹ : Semiring S'
inst✝ : Algebra R' S'
i : R' →+* R
j : S →+* S'
hi : Injective ⇑i
hj : Injective ⇑j
hc : (j.comp (algebraMap R S)).comp i = algebraMap R' S'
r : R'
x✝ : S
this : ((j.comp (algebraMap R S)).comp i) r = (algebraMap R' S') r
⊢ ↑j (i r • x✝) = r • ↑j x✝

Tactic:
simp only [RingHom.coe_comp, comp_apply] at this

Goal state after:
R : Type w
S : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring S
inst✝³ : Algebra R S
R' : Type w'
S' : Type v'
inst✝² : CommSemiring R'
inst✝¹ : Semiring S'
inst✝ : Algebra R' S'
i : R' →+* R
j : S →+* S'
hi : Injective ⇑i
hj : Injective ⇑j
hc : (j.comp (algebraMap R S)).comp i = algebraMap R' S'
r : R'
x✝ : S
this : j ((algebraMap R S) (i r)) = (algebraMap R' S') r
⊢ ↑j (i r • x✝) = r • ↑j x✝
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type w
S : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring S
inst✝³ : Algebra R S
R' : Type w'
S' : Type v'
inst✝² : CommSemiring R'
inst✝¹ : Semiring S'
inst✝ : Algebra R' S'
i : R →+* R'
j : S →+* S'
hi : Surjective ⇑i
hj : Injective ⇑j
hc : (algebraMap R' S').comp i = j.comp (algebraMap R S)
r : R
x✝ : S
this : ((algebraMap R' S').comp i) r = (j.comp (algebraMap R S)) r
⊢ ↑j (r • x✝) = i r • ↑j x✝

Tactic:
simp only [RingHom.coe_comp, comp_apply] at this

Goal state after:
R : Type w
S : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring S
inst✝³ : Algebra R S
R' : Type w'
S' : Type v'
inst✝² : CommSemiring R'
inst✝¹ : Semiring S'
inst✝ : Algebra R' S'
i : R →+* R'
j : S →+* S'
hi : Surjective ⇑i
hj : Injective ⇑j
hc : (algebraMap R' S').comp i = j.comp (algebraMap R S)
r : R
x✝ : S
this : (algebraMap R' S') (i r) = j ((algebraMap R S) r)
⊢ ↑j (r • x✝) = i r • ↑j x✝
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
⊢ Module.rank R ↥s ≤ Module.rank R M

Tactic:
rw [← rank_top R M]

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
⊢ Module.rank R ↥s ≤ Module.rank R ↥⊤
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ∞
⊢ s.encard = k + 1 ↔ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.encard = k

Tactic:
by
  refine ⟨fun h ↦ ?_, ?_⟩
  · obtain ⟨a, ha⟩ := nonempty_of_encard_ne_zero (s := s) (by simp [h])
    refine ⟨a, s \ {a}, fun h ↦ h.2 rfl, by rwa [insert_sdiff_singleton, insert_eq_of_mem], ?_⟩
    rw [encard_sdiff_singleton_of_mem ha, h,
      (ENat.addLECancellable_of_ne_top ENat.one_ne_top).add_tsub_cancel_right]
  rintro ⟨a, t, h, rfl, rfl⟩
  rw [encard_insert_of_notMem h]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
f' : Fin n → α := fun i ↦ f ↑i ⋯
himage : s = f' '' univ
⊢ s.ncard = n

Tactic:
← Fintype.card_fin n,

Goal state after:
α : Type u_1
s : Set α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
f' : Fin n → α := fun i ↦ f ↑i ⋯
himage : s = f' '' univ
⊢ s.ncard = Fintype.card (Fin n)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Infinite
this : Infinite ↑s
t' : Finset ↑s
⊢ ∃ t ⊆ s, t.Finite ∧ t.ncard = t'.card

Tactic:
refine ⟨Subtype.val '' (t' : Set s), by simp, Finite.image _ (by simp), ?_⟩

Goal state after:
α : Type u_1
s : Set α
hs : s.Infinite
this : Infinite ↑s
t' : Finset ↑s
⊢ (Subtype.val '' ↑t').ncard = t'.card
Module: Mathlib.LinearAlgebra.Quotient.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
x y : M
⊢ -x + y ∈ p.toAddSubgroup ↔ -(x - y) ∈ p

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
x y : M
⊢ -x + y ∈ p.toAddSubgroup ↔ -(x + -y) ∈ p
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
hb : IsMin b
⊢ Ioc a (pred b) = Ioo a b

pp: case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
hb : ¬IsMin b
⊢ Ioc a (pred b) = Ioo a b

Tactic:
· rw [Ioc_eq_empty (hb.mono <| pred_le _).not_lt, Ioo_eq_empty hb.not_lt]

Goal state after:
case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
hb : ¬IsMin b
⊢ Ioc a (pred b) = Ioo a b
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
⊢ (p.mapQ q f h).range = map q.mkQ f.range

Tactic:
mapQ,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
⊢ (p.liftQ (q.mkQ ∘ₛₗ f) ⋯).range = map q.mkQ f.range
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : a < b
⊢ insert (pred b) (Ico a (pred b)) = Ico a b

Tactic:
rw [Ico_insert_right (le_pred_of_lt h), Icc_pred_right_of_not_isMin h.not_isMin]

Goal state after:
Module: Mathlib.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a : α
⊢ ↑(Ico a (succ b)) = ↑(Icc a b)

Tactic:
simpa using Set.Ico_succ_right_eq_Icc_of_not_isMax hb _

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f : M →ₗ[R] M₂
I : Type u_1
x✝ : I → M₂
hx : x✝ ∈ Submodule.pi Set.univ fun x ↦ f.range
⊢ x✝ ∈ (f.compLeft I).range

Tactic:
by
    choose y hy using hx
    exact ⟨fun i => y i trivial, funext fun i => hy i trivial⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f : M →ₗ[R] M₂
⊢ f.graph = (id.prod f).range

Tactic:
ext x
  exact ⟨fun hx => ⟨x.1, Prod.ext rfl hx.symm⟩, fun ⟨u, hu⟩ => hu ▸ rfl⟩

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
hn : IsMin i
⊢ Iio i = ∅

Tactic:
rwa [← Finset.coe_eq_empty, coe_Iio, Set.Iio_eq_empty_iff]

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝¹ : CancelCommMonoid A
inst✝ : HasMulAntidiagonal A
p q : A × A
n : A
hp : p ∈ mulAntidiagonal n
hq : q ∈ mulAntidiagonal n
⊢ p = q ↔ p.2 = q.2

Tactic:
rw [← Prod.swap_inj]

Goal state after:
A : Type u_1
inst✝¹ : CancelCommMonoid A
inst✝ : HasMulAntidiagonal A
p q : A × A
n : A
hp : p ∈ mulAntidiagonal n
hq : q ∈ mulAntidiagonal n
⊢ p.swap = q.swap ↔ p.2 = q.2
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasAntidiagonal A
a : A
p : Multiplicative A × Multiplicative A
⊢ p ∈ mulAntidiagonal (ofAdd a) ↔ (toAdd p.1, toAdd p.2) ∈ antidiagonal a

Tactic:
simp only [mem_mulAntidiagonal, mem_antidiagonal]
  rw [Multiplicative.ext_iff, toAdd_mul, toAdd_ofAdd]

Goal state after:
Module: Mathlib.Data.List.NatAntidiagonal

Goal state before:
pp: n : ℕ
x : ℕ × ℕ
⊢ x ∈ antidiagonal n ↔ x.fst + x.snd = n

Tactic:
by
  rcases x with ⟨x, y⟩
  simp [antidiagonal]
  grind

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

Goal state before:
pp: case succ
α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsPrime
r : α
n : ℕ
ih : r ^ n ∈ I → r ∈ I
H : r ^ n * r ∈ I
⊢ r ∈ I

Tactic:
exact Or.casesOn (hI.mem_or_mem H) ih id

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

Goal state before:
pp: α : Type u
inst✝² : Semiring α
I : Ideal α
inst✝¹ : I.IsTwoSided
inst✝ : I.IsPrime
x y : α
hx : x ∉ I
⊢ x * y ∈ I ↔ y ∈ I

Tactic:
by
  grind [Ideal.IsPrime.mul_mem_iff_mem_or_mem]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
n : ℕ
⊢ (x - y) ^ n = ∑ m ∈ range (n + 1), (-1) ^ (m + n) * x ^ m * y ^ (n - m) * ↑(n.choose m)

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y : R
n : ℕ
⊢ (x + -y) ^ n = ∑ m ∈ range (n + 1), (-1) ^ (m + n) * x ^ m * y ^ (n - m) * ↑(n.choose m)
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
a : α
h2 : IsUnit a
x : α
⊢ span {x * a} = span {x}

Tactic:
by rw [mul_comm, span_singleton_mul_left_unit h2]

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

Goal state before:
pp: case isUnit_or_isUnit
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
⊢ ∀ ⦃a_1 b : α⦄, a = a_1 * b → IsUnit a_1 ∨ IsUnit b

Tactic:
intro u v ha

Goal state after:
case isUnit_or_isUnit
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
u v : α
ha : a = u * v
⊢ IsUnit u ∨ IsUnit v
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
y : I → M
hy : ∀ (i : I), f (y i) = x i
i : I
⊢ i ∈ x.support ↔ y i ≠ 0

Tactic:
constructor
    <;> contrapose
    <;> simp_all +contextual [← hy, map_zero, LinearMap.ker_eq_bot'.1 hf]

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
p : ι → Prop
l : Filter α
h : ∀ {s : Set α}, s ∈ l ↔ ∃ i, p i ∧ s ∈ f i
⊢ l = ⨅ i, ⨅ (_ : p i), f i

Tactic:
iInf_subtype'

Goal state after:
α : Type u
ι : Sort x
f : ι → Filter α
p : ι → Prop
l : Filter α
h : ∀ {s : Set α}, s ∈ l ↔ ∃ i, p i ∧ s ∈ f i
⊢ l = ⨅ x, f ↑x
Module: Mathlib.Order.Filter.AtTopBot.Disjoint

Goal state before:
pp: case neg
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : ¬x ≤ y
⊢ Disjoint atBot atTop

Tactic:
refine disjoint_of_disjoint_of_mem ?_ (Iic_mem_atBot y) (Ici_mem_atTop x)
    exact Iic_disjoint_Ici.2 hle

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

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommSemigroup β
mul : Mul α := e.mul
⊢ CommSemigroup α

Tactic:
apply e.injective.commSemigroup _

Goal state after:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommSemigroup β
mul : Mul α := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y
Module: Mathlib.Algebra.NoZeroSMulDivisors.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMul R M
⊢ NoZeroSMulDivisors R M ↔ ∀ (r : R), r ≠ 0 → ∀ (m : M), r • m = 0 → m = 0

Tactic:
noZeroSMulDivisors_iff,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMul R M
⊢ (∀ {c : R} {x : M}, c • x = 0 → c = 0 ∨ x = 0) ↔ ∀ (r : R), r ≠ 0 → ∀ (m : M), r • m = 0 → m = 0
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : LE α
⊢ IsCofinal ∅ ↔ IsEmpty α

Tactic:
refine ⟨fun h ↦ ⟨fun a ↦ ?_⟩, fun h ↦ .of_isEmpty⟩

Goal state after:
α : Type u_1
inst✝ : LE α
h : IsCofinal ∅
a : α
⊢ False
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
S : Type u_3
P : Type u_4
inst✝⁴ : Semiring S
inst✝³ : AddCommMonoid P
inst✝² : Module S P
σ : R →+* S
inst✝¹ : RingHomSurjective σ
inst✝ : Module.Finite R M
f : M →ₛₗ[σ] P
⊢ f.range.FG

Tactic:
LinearMap.range_eq_map

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
S : Type u_3
P : Type u_4
inst✝⁴ : Semiring S
inst✝³ : AddCommMonoid P
inst✝² : Module S P
σ : R →+* S
inst✝¹ : RingHomSurjective σ
inst✝ : Module.Finite R M
f : M →ₛₗ[σ] P
⊢ (map f ⊤).FG
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
x✝ : cof α = 0
⊢ IsEmpty α

Tactic:
obtain ⟨s, hs, hs'⟩ := exists_cof_eq α

Goal state after:
α : Type u
inst✝ : Preorder α
x✝ : cof α = 0
s : Set α
hs : IsCofinal s
hs' : #↑s = cof α
⊢ IsEmpty α
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: case refine_1
α : Type u
inst✝ : Preorder α
h : cof α = 1
⊢ ∃ x, IsTop x

Tactic:
obtain ⟨s, hs, hs'⟩ := exists_cof_eq α

Goal state after:
case refine_1
α : Type u
inst✝ : Preorder α
h : cof α = 1
s : Set α
hs : IsCofinal s
hs' : #↑s = cof α
⊢ ∃ x, IsTop x
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : PosSMulMono α β
inst✝ : SMulPosMono α β
hab : 0 < a • b
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
obtain ha | rfl | ha := lt_trichotomy a 0

Goal state after:
case inl
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : PosSMulMono α β
inst✝ : SMulPosMono α β
hab : 0 < a • b
ha : a < 0
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

case inr.inl
α : Type u_1
β : Type u_2
b : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : PosSMulMono α β
inst✝ : SMulPosMono α β
hab : 0 < 0 • b
⊢ 0 < 0 ∧ 0 < b ∨ 0 < 0 ∧ b < 0

case inr.inr
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : PosSMulMono α β
inst✝ : SMulPosMono α β
hab : 0 < a • b
ha : 0 < a
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
h : cof α < ℵ₀
⊢ cof α ≤ 1

Tactic:
obtain ⟨s, hs, hs'⟩ := exists_cof_eq α

Goal state after:
α : Type u
inst✝ : LinearOrder α
h : cof α < ℵ₀
s : Set α
hs : IsCofinal s
hs' : #↑s = cof α
⊢ cof α ≤ 1