mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
a : α
v : Vector α n
hp : ∀ (x : α), x ∈ (a ::ᵥ v).toList → p x
⊢ p a

Tactic:
by
      simp only [Nat.succ_eq_add_one, toList_cons, List.mem_cons, forall_eq_or_imp] at hp
      exact hp.1

Goal state after:
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
h : a ≠ b
⊢ ((if ¬a = b then count b ↑m else 0) + if a = b then count a ↑m else 0) = count b ↑m

Tactic:
· rw [if_pos h, if_neg h, add_zero]

Goal state after:
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type u_1
inst✝ : Denumerable α
⊢ ofNat (List α) 0 = []

Tactic:
rw [← @encode_list_nil α, ofNat_encode]

Goal state after:
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case mk.mk.mk
α : Type u_1
n : ℕ
a : α
val✝² : List α
property✝ : val✝².length = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : ⟨val✝¹, isLt✝¹⟩ ≠ ⟨val✝, isLt✝⟩
⊢ (val✝².set val✝¹ a)[val✝] = val✝²[val✝]

Tactic:
rw [List.getElem_set_of_ne]

Goal state after:
case mk.mk.mk.h
α : Type u_1
n : ℕ
a : α
val✝² : List α
property✝ : val✝².length = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : ⟨val✝¹, isLt✝¹⟩ ≠ ⟨val✝, isLt✝⟩
⊢ val✝¹ ≠ val✝
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
⊢ sSup (Iio x) = x ↔ IsSuccPrelimit x

Tactic:
sSup_Iio_eq_self_iff_isSuccPrelimit

Goal state after:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
⊢ IsSuccPrelimit x ↔ IsSuccPrelimit x
Module: Mathlib.SetTheory.Cardinal.Defs

Goal state before:
pp: ι : Type u_1
f : ι → Cardinal.{u}
⊢ prod f = 0 ↔ ∃ i, f i = 0

Tactic:
lift f to ι → Type u using fun _ => trivial

Goal state after:
ι : Type u_1
f : ι → Type u
⊢ (prod fun i ↦ #(f i)) = 0 ↔ ∃ i, (fun i ↦ #(f i)) i = 0
Module: Mathlib.SetTheory.Cardinal.Defs

Goal state before:
pp: ι : Type u_1
f : ι → Type u
⊢ (prod fun i ↦ #(f i)) = 0 ↔ ∃ i, (fun i ↦ #(f i)) i = 0

Tactic:
simp only [mk_eq_zero_iff, ← mk_pi, isEmpty_pi]

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝² : Std.Trichotomous s
inst✝¹ : Std.Irrefl s
inst✝ : IsWellFounded α r
f g : r ≼i s
a b : α
IH : ∀ (y : α), r y b → f y = g y
x : β
⊢ (∃ a', f a' = x ∧ r a' b) ↔ s x (g b)

Tactic:
g.exists_eq_iff_rel

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝² : Std.Trichotomous s
inst✝¹ : Std.Irrefl s
inst✝ : IsWellFounded α r
f g : r ≼i s
a b : α
IH : ∀ (y : α), r y b → f y = g y
x : β
⊢ (∃ a', f a' = x ∧ r a' b) ↔ ∃ a', g a' = x ∧ r a' b
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case right
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ωSup c ∈ lowerBounds (upperBounds (Set.range ⇑c))

Tactic:
simp only [lowerBounds, upperBounds, Set.mem_range, forall_exists_index,
      forall_apply_eq_imp_iff, Set.mem_ofPred_eq]

Goal state after:
case right
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ∀ ⦃a : α⦄, (∀ (a_1 : ℕ), c a_1 ≤ a) → ωSup c ≤ a
Module: Mathlib.Order.Zorn

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : Preorder α
a : α
ih : ∀ c ⊆ Ici a, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub
x : α
hax : a ≤ x
c : Set α
hca : c ⊆ Ici a
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
⊢ ∃ ub ∈ Ici a, ∀ z ∈ c, z ≤ ub

Tactic:
have ⟨ub, hub⟩ := ih c hca hc y hy
    exact ⟨ub, (hca hy).trans (hub y hy), hub⟩

Goal state after:
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
hc₁ : ChainClosure r c₁
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
⊢ c₁ ⊆ c₂

Tactic:
by
  induction hc₁ with
  | succ hc₁ h => exact (chainClosure_succ_total hc₁ hc₂ h).elim (fun h => h ▸ hc.subset) id
  | union _ ih => exact sUnion_subset ih

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
⊢ g' '' sᶜ = (f '' s)ᶜ

Tactic:
rw [← hns, g'g.image_image]

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

Goal state before:
pp: case pos
c : Cardinal.{u}
h : c = 0
⊢ 0 ^ c ≤ 1

Tactic:
rw [h, power_zero]

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

Goal state before:
pp: case neg
c : Cardinal.{u}
h : ¬c = 0
⊢ 0 ^ c ≤ 1

Tactic:
rw [zero_power h]

Goal state after:
case neg
c : Cardinal.{u}
h : ¬c = 0
⊢ 0 ≤ 1
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: a : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} a ≤ ↑n ↔ a ≤ ↑n

Tactic:
← lift_natCast.{v, u},

Goal state after:
a : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} a ≤ lift.{v, u} ↑n ↔ a ≤ ↑n
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: n : ℕ
a : Cardinal.{u}
⊢ ↑n ≤ lift.{v, u} a ↔ ↑n ≤ a

Tactic:
← lift_natCast.{v, u},

Goal state after:
n : ℕ
a : Cardinal.{u}
⊢ lift.{v, u} ↑n ≤ lift.{v, u} a ↔ ↑n ≤ a
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: a : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} a < ↑n ↔ a < ↑n

Tactic:
← lift_natCast.{v, u},

Goal state after:
a : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} a < lift.{v, u} ↑n ↔ a < ↑n
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: n : ℕ
a : Cardinal.{u}
⊢ ↑n < lift.{v, u} a ↔ ↑n < a

Tactic:
← lift_natCast.{v, u},

Goal state after:
n : ℕ
a : Cardinal.{u}
⊢ lift.{v, u} ↑n < lift.{v, u} a ↔ ↑n < a
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: c : Cardinal.{u}
d : Cardinal.{v}
h : ∀ (n : ℕ), ↑n ≤ c ↔ ↑n ≤ d
⊢ toNat c = toNat d

Tactic:
have h' := forall_congr' h

Goal state after:
c : Cardinal.{u}
d : Cardinal.{v}
h : ∀ (n : ℕ), ↑n ≤ c ↔ ↑n ≤ d
h' : (∀ (a : ℕ), ↑a ≤ c) ↔ ∀ (a : ℕ), ↑a ≤ d
⊢ toNat c = toNat d
Module: Mathlib.Algebra.Ring.CompTypeclasses

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝² : Semiring R₁
inst✝¹ : Semiring R₂
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝ : RingHomInvPair σ σ'
x : R₁
⊢ σ' (σ x) = x

Tactic:
by
  rw [← RingHom.comp_apply, comp_eq]
  simp

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

Goal state before:
pp: α : Type u
s : Set α
⊢ #↑(ULift.down ⁻¹' s) = #(ULift.{v, u} ↑s)

Tactic:
Cardinal.eq

Goal state after:
α : Type u
s : Set α
⊢ Nonempty (↑(ULift.down ⁻¹' s) ≃ ULift.{v, u} ↑s)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case neg
α : Type u
s : Set α
a : α
h : a ∉ s
⊢ #↑(insert a s) ≤ #↑s + 1

Tactic:
rw [mk_insert h]

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

Goal state before:
pp: α : Type u_1
h : 3 ≤ #α
x y : α
⊢ ∃ z, z ≠ x ∧ z ≠ y

Tactic:
have : ↑(3 : ℕ) ≤ #α := by simpa using h
  have : ↑(2 : ℕ) < #α := by rwa [← natCast_add_one_le_iff, ← Nat.cast_add_one]
  have := exists_notMem_of_length_lt [x, y] this
  simpa [not_or] using this

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

Goal state before:
pp: R✝ : Type u
S : Type v
A✝ : Type w
B : Type u_1
inst✝⁶ : CommSemiring R✝
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
inst✝² : Semiring B
inst✝¹ : Algebra R✝ B
R : Type ?u.22
A : Type ?u.24
x✝¹ : CommSemiring R
x✝ : Semiring A
inst✝ : Algebra R A
⊢ ∀ (r s : R) (x : A), (r + s) • x = r • x + s • x

Tactic:
simp [smul_def', add_mul]

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

Goal state before:
pp: M : Type u_8
M₂ : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
⊢ Injective toNatLinearMap

Tactic:
intro f g h

Goal state after:
M : Type u_8
M₂ : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
f g : M →+ M₂
h : f.toNatLinearMap = g.toNatLinearMap
⊢ f = g
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: M : Type u_8
M₂ : Type u_10
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup M₂
⊢ Injective toIntLinearMap

Tactic:
intro f g h

Goal state after:
M : Type u_8
M₂ : Type u_10
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup M₂
f g : M →+ M₂
h : f.toIntLinearMap = g.toIntLinearMap
⊢ f = g
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: case succ
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
k : ℕ
ih : (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)
⊢ g₂ ∘ₛₗ f ∘ₛₗ (g ^ k) = f ∘ₛₗ (g * g ^ k)

Tactic:
← LinearMap.comp_assoc,

Goal state after:
case succ
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
k : ℕ
ih : (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)
⊢ (g₂ ∘ₛₗ f) ∘ₛₗ (g ^ k) = f ∘ₛₗ (g * g ^ k)
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ (∀ (x y : ↥p), x = y) ↔ ∀ x ∈ p, x = 0

Tactic:
refine ⟨fun h x hx ↦ by simpa using h ⟨x, hx⟩ ⟨0, p.zero_mem⟩,
    fun h ⟨x, hx⟩ ⟨y, hy⟩ ↦ by simp [h x hx, h y hy]⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S T : Submodule R M
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T

Tactic:
have : T ≤ S ⊔ T := le_sup_right

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S T : Submodule R M
this : T ≤ S ⊔ T
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝⁴ : FunLike F α β
inst✝³ : SupSet α
inst✝² : SupSet β
inst✝¹ : SupSet γ
inst✝ : SupSet δ
f : sSupHom β γ
g : sSupHom α β
s : Set α
⊢ (⇑f ∘ ⇑g) (sSup s) = sSup (⇑f ∘ ⇑g '' s)

Tactic:
by rw [comp_apply, map_sSup, map_sSup, Set.image_image]; simp only [Function.comp]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
⊢ Disjoint p f.ker ↔ Set.InjOn ⇑f ↑p

Tactic:
rw [disjoint_ker, Set.injOn_iff_map_eq_zero]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
i : Injective ⇑f
p : Submodule R M
x : ↥(map f p)
⊢ f ↑((equivMapOfInjective f i p).symm ((equivMapOfInjective f i p) ((equivMapOfInjective f i p).symm x))) =
    f ↑((equivMapOfInjective f i p).symm x)

Tactic:
i.eq_iff,

Goal state after:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
i : Injective ⇑f
p : Submodule R M
x : ↥(map f p)
⊢ ↑((equivMapOfInjective f i p).symm ((equivMapOfInjective f i p) ((equivMapOfInjective f i p).symm x))) =
    ↑((equivMapOfInjective f i p).symm x)
Module: Mathlib.Algebra.GroupWithZero.Center

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
x✝¹ x✝ : M₀
⊢ 0 * (x✝¹ * x✝) = 0 * x✝¹ * x✝

Tactic:
rw [zero_mul, zero_mul, zero_mul]

Goal state after:
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocSemiring M
n : ℕ
x✝¹ x✝ : M
⊢ x✝¹ * x✝ * ↑n = x✝¹ * (x✝ * ↑n)

Tactic:
by
    induction n with
    | zero => rw [Nat.cast_zero, mul_zero, mul_zero, mul_zero]
    | succ n ihn => rw [Nat.cast_succ, mul_add, ihn, mul_add, mul_add, mul_one, mul_one]

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
S T : Subsemigroup M
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T

Tactic:
have : T ≤ S ⊔ T := le_sup_right

Goal state after:
M : Type u_2
inst✝ : Mul M
S T : Subsemigroup M
this : T ≤ S ⊔ T
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
S T : Subring R
h : S ≤ T
x : ↥S
⊢ ↑((inclusion h) x) = ↑x

Tactic:
by simp [Subring.inclusion]

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case cons.inl.cons
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ x ∈ tl, x ∈ s) → C tl.prod
HL' : hd ∈ s ∧ ∀ x ∈ tl, x ∈ s
⊢ C (hd :: tl).prod

Tactic:
List.prod_cons

Goal state after:
case cons.inl.cons
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ x ∈ tl, x ∈ s) → C tl.prod
HL' : hd ∈ s ∧ ∀ x ∈ tl, x ∈ s
⊢ C (hd * tl.prod)
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ IsPrimal (Associates.mk a) ↔ IsPrimal a

Tactic:
simp_rw [IsPrimal, forall_associated, mk_surjective.exists, mk_mul_mk, mk_dvd_mk]

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ (∀ (a_1 a_2 : M), a ∣ a_1 * a_2 → ∃ x x_1, x ∣ a_1 ∧ x_1 ∣ a_2 ∧ Associates.mk a = Associates.mk (x * x_1)) ↔
    ∀ ⦃b c : M⦄, a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ Irreducible (Associates.mk a) ↔ Irreducible a

Tactic:
simp only [irreducible_iff, isUnit_mk, forall_associated, isUnit_mk, mk_mul_mk,
    mk_eq_mk_iff_associated, Associated.comm (x := a)]
  apply Iff.rfl.and
  constructor
  · rintro h x y rfl
    exact h _ _ <| .refl _
  · rintro h x y ⟨u, rfl⟩
    simpa using h (mul_assoc _ _ _)

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f g : M →ₛₗ[τ₁₂] M₂
⊢ (f + g).range ≤ f.range ⊔ g.range

Tactic:
rintro - ⟨_, rfl⟩

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f g : M →ₛₗ[τ₁₂] M₂
w✝ : M
⊢ (f + g) w✝ ∈ f.range ⊔ g.range
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝ : Preorder α
⊢ Function.Injective fun c ↦ ⇑c.toOrderHom

Tactic:
by rintro ⟨⟩ ⟨⟩ h; obtain rfl := DFunLike.ext' h; congr with x; simp_all

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
b c : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x y : α
hcodisjoint : Codisjoint x y
x✝ : ↑(Ici (x ⊓ y))
hx : x ∈ Ici (x ⊓ y)
⊢ ∃ b, x ⊓ ↑b = x ⊓ y ∧ Codisjoint x ↑b

Tactic:
exact ⟨⟨y, inf_le_right⟩, rfl, hcodisjoint⟩

Goal state after:
Module: Mathlib.Order.Interval.Set.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : α
⊢ ⇑e '' Ioc a b = Ioc (e a) (e b)

Tactic:
by
  rw [e.image_eq_preimage_symm, e.symm.preimage_Ioc, e.symm_symm]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
β : ι → Type u_5
t : (i : ι) → β i → α
ht : ∀ (i : ι), iSupIndep (t i)
⊢ InjOn (fun b ↦ ⨅ i, t i (b i)) {b | ⨅ i, t i (b i) ≠ ⊥}

Tactic:
intro b₁ hb₁ b₂ hb₂ h_eq

Goal state after:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
β : ι → Type u_5
t : (i : ι) → β i → α
ht : ∀ (i : ι), iSupIndep (t i)
b₁ : (i : ι) → β i
hb₁ : b₁ ∈ {b | ⨅ i, t i (b i) ≠ ⊥}
b₂ : (i : ι) → β i
hb₂ : b₂ ∈ {b | ⨅ i, t i (b i) ≠ ⊥}
h_eq : (fun b ↦ ⨅ i, t i (b i)) b₁ = (fun b ↦ ⨅ i, t i (b i)) b₂
⊢ b₁ = b₂
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f g : ι → α
h₂ : iSup f = ⊤
h₃ : f ≤ g
i : ι
h₁ : Disjoint (⨆ j, ⨆ (_ : j ≠ i), f j) (g i)
⊢ f i ⊔ ⨆ j, ⨆ (_ : j ≠ i), f j = ⊤

Tactic:
← iSup_split_single f i,

Goal state after:
α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f g : ι → α
h₂ : iSup f = ⊤
h₃ : f ≤ g
i : ι
h₁ : Disjoint (⨆ j, ⨆ (_ : j ≠ i), f j) (g i)
⊢ ⨆ i, f i = ⊤
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case refine_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ x ∈ S, ¬t.sup id < x
y : α
hy : y ∈ s
⊢ y ≤ t.sup id

Tactic:
classical
    rw [eq_of_le_of_not_lt (Finset.sup_mono (t.subset_insert y))
        (hm _ ⟨insert y t, by simp [Set.insert_subset_iff, hy, ht₁]⟩)]
    simp

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

Goal state before:
pp: case mpr.add
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
S : Set M
f g : ↥(span R S) →ₗ[R] N
h : ∀ (s : ↑S), f ⟨↑s, ⋯⟩ = g ⟨↑s, ⋯⟩
x✝ x y : M
hx : x ∈ span R S
hy : y ∈ span R S
hx' : f ⟨x, hx⟩ = g ⟨x, hx⟩
hy' : f ⟨y, hy⟩ = g ⟨y, hy⟩
⊢ f ⟨x, hx⟩ + f ⟨y, hy⟩ = g ⟨x + y, ⋯⟩

Tactic:
g.map_add ⟨x, hx⟩ ⟨y, hy⟩

Goal state after:
case mpr.add
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
S : Set M
f g : ↥(span R S) →ₗ[R] N
h : ∀ (s : ↑S), f ⟨↑s, ⋯⟩ = g ⟨↑s, ⋯⟩
x✝ x y : M
hx : x ∈ span R S
hy : y ∈ span R S
hx' : f ⟨x, hx⟩ = g ⟨x, hx⟩
hy' : f ⟨y, hy⟩ = g ⟨y, hy⟩
⊢ f ⟨x, hx⟩ + f ⟨y, hy⟩ = g ⟨x, hx⟩ + g ⟨y, hy⟩
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: α : Type u_1
G : Type u_6
inst✝ : Group G
s t : Set α
h : s ⊆ t
f : α → G
⊢ (t \ s).mulIndicator f * s.mulIndicator f = t.mulIndicator f

Tactic:
by
    rw [Pi.mul_def, ← mulIndicator_union_of_disjoint, sdiff_union_self,
      union_eq_self_of_subset_right h]
    exact disjoint_sdiff_self_left

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
f g : ι → R
s : Finset ι
a : (a : ι) → a ∈ s → Prop
x✝ : a ∈ s.pi fun x ↦ {True, False}
⊢ (∏ a_1 ∈ s.attach, if a ↑a_1 ⋯ then f ↑a_1 else g ↑a_1) =
    (∏ a ∈ s with ∃ (h : a ∈ s), a a h, f a) * ∏ a ∈ s \ {a_1 ∈ s | ∃ (h : a_1 ∈ s), a a_1 h}, g a

Tactic:
by
          simp only [prod_ite, filter_attach', prod_map, Function.Embedding.coeFn_mk,
            Subtype.map_coe, id_eq, prod_attach]
          congr 2 with x
          simp only [mem_filter, mem_sdiff, not_and, not_exists, and_congr_right_iff]
          tauto

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : Module.End R R
h : f (f 1) = f 1
r : R
⊢ f (f r) = f r

Tactic:
rw [← mul_one r, ← smul_eq_mul, map_smul, map_smul, h]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
⊢ (⋂ i, s i).mulIndicator f x = ⨅ i, (s i).mulIndicator f x

Tactic:
by_cases hx : x ∈ ⋂ i, s i
  · simp_all
  · rw [mulIndicator_of_notMem hx]
    simp only [mem_iInter, not_forall] at hx
    rcases hx with ⟨j, hj⟩
    refine le_antisymm (by simp only [← h1, le_iInf_iff, bot_le, forall_const]) ?_
    simpa [mulIndicator_of_notMem hj] using (iInf_le (fun i ↦ (s i).mulIndicator f) j) x

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: case neg
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
h✝ : ¬i ∈ s
⊢ 0 = 0 * g i

Tactic:
rw [zero_mul]

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

Goal state before:
pp: case single
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
a : Option α
m : M
⊢ (single a m).prod b = b none ((single a m) none) * (single a m).some.prod fun a ↦ b (Option.some a)

Tactic:
cases a <;> simp [h_zero]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : Type u_8
N : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
s✝ : Finset ι
g : ι → α →₀ M
h : α → M → N
h_zero : ∀ (a : α), h a 0 = 1
h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
a : ι
s : Finset ι
has : a ∉ s
ih : ∏ i ∈ s, (g i).prod h = (∑ i ∈ s, g i).prod h
⊢ ∏ i ∈ cons a s has, (g i).prod h = (∑ i ∈ cons a s has, g i).prod h

Tactic:
by
    rw [prod_cons, ih, sum_cons, prod_add_index' h_zero h_add]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: case mk
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
l : List ι
⊢ max (↑(List.map f l)).prod (↑(List.map g l)).prod ≤ (↑(List.map (fun i ↦ max (f i) (g i)) l)).prod

Tactic:
Multiset.prod_coe

Goal state after:
case mk
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
l : List ι
⊢ max (List.map f l).prod (List.map g l).prod ≤ (List.map (fun i ↦ max (f i) (g i)) l).prod
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: case mk
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
l : List ι
⊢ (↑(List.map (fun i ↦ min (f i) (g i)) l)).prod ≤ min (↑(List.map f l)).prod (↑(List.map g l)).prod

Tactic:
Multiset.prod_coe

Goal state after:
case mk
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
l : List ι
⊢ (List.map (fun i ↦ min (f i) (g i)) l).prod ≤ min (List.map f l).prod (List.map g l).prod
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset

Goal state before:
pp: case inl
ι : Type u_1
s : Finset ι
M : Type u_4
inst✝³ : CommMonoidWithZero M
inst✝² : LinearOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
i : ι
hi : i ∈ s
f : ι → M
hf : f i < 0
⊢ f i ≤ ∏ i ∈ s, max (f i) 1

Tactic:
exact (hf.trans_le <| prod_nonneg fun _ _ ↦ le_sup_of_le_right zero_le_one).le

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List

Goal state before:
pp: R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
ι : Type u_2
f g : ι → R
a : ι
s : List ι
hind : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
this : MulPosMono R
⊢ a ∈ a :: s

Tactic:
simp only [mem_cons, true_or]

Goal state after: