mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
f : β → γ
g : α → Part β
hg : Antitone g
⊢ Antitone fun x ↦ map f (g x)

Tactic:
by
  simpa only [← bind_some_eq_map] using hg.partBind antitone_const

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
⊢ ∃ z ∈ c, ¬f z ≤ y

Tactic:
by_contra! h

Goal state after:
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
h : ∀ z ∈ c, f z ≤ y
⊢ False
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 : α
hub : ∀ z ∈ c, z ≤ ub
⊢ ∃ ub ∈ Ici a, ∀ z ∈ c, z ≤ ub

Tactic:
exact ⟨ub, (hca hy).trans (hub y hy), hub⟩

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

Goal state before:
pp: a : Cardinal.{u}
⊢ lift.{v, u} (succ a) ≤ succ (lift.{v, u} a)

Tactic:
by_contra! h

Goal state after:
a : Cardinal.{u}
h : succ (lift.{v, u} a) < lift.{v, u} (succ a)
⊢ False
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: c : Cardinal.{u_1}
h : c < ℵ₀
⊢ ↑(toNat c) = c

Tactic:
lift c to ℕ using h
  rw [toNat_natCast]

Goal state after:
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: M : Type u_3
inst✝ : SubtractionMonoid M
n : ℤ
⊢ IsSMulRegular M n.natAbs ↔ IsSMulRegular M n

Tactic:
simp_rw [IsSMulRegular, Function.Injective]
  conv_rhs => rw [← n.sign_mul_natAbs]
  obtain h | h | h := n.sign_trichotomy
  · simp [h]
  · simp [Int.sign_eq_zero_iff_zero.mp h]
  · simp [h, neg_zsmul]

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

Goal state before:
pp: s : Set Cardinal.{v}
⊢ lift.{u, v} (sInf s) = sInf (lift.{u, v} '' s)

Tactic:
rcases eq_empty_or_nonempty s with (rfl | hs)

Goal state after:
case inl
⊢ lift.{u, v} (sInf ∅) = sInf (lift.{u, v} '' ∅)

case inr
s : Set Cardinal.{v}
hs : s.Nonempty
⊢ lift.{u, v} (sInf s) = sInf (lift.{u, v} '' s)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
hf : BddAbove (range f)
g : Cardinal.{v} → Cardinal.{max v w}
⊢ BddAbove (range (g ∘ f))

Tactic:
rw [range_comp]
  exact bddAbove_image g hf

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
hf : Injective f
⊢ lift.{v, u} #α ≤ lift.{u, v} #β

Tactic:
by
  rw [← Cardinal.mk_range_eq_of_injective hf]
  exact Cardinal.lift_le.2 (Cardinal.mk_set_le _)

Goal state after:
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
m : M
a : α
| SMul.smul m a

Tactic:
rw [← hN.one_smul a]

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
m : M
a : α
| SMul.smul m (1 • a)
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
x✝ : MulAction N α
m : M
a : α
| SMul.smul m a

Tactic:
rw [← hN.one_smul a]

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
x✝ : MulAction N α
m : M
a : α
| SMul.smul m (1 • a)
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
X : Type u_5
inst✝⁶ : SMul M' X
Y : Type u_6
inst✝⁵ : SMul M' Y
F : Type u_8
inst✝⁴ : FunLike F X Y
inst✝³ : MulOneClass X
inst✝² : SMul X Y
inst✝¹ : IsScalarTower M' X Y
inst✝ : MulActionHomClass F X X Y
f : F
m : M'
x : X
⊢ m • x • f 1 = id m • f x

Tactic:
← map_smul,

Goal state after:
M' : Type u_1
X : Type u_5
inst✝⁶ : SMul M' X
Y : Type u_6
inst✝⁵ : SMul M' Y
F : Type u_8
inst✝⁴ : FunLike F X Y
inst✝³ : MulOneClass X
inst✝² : SMul X Y
inst✝¹ : IsScalarTower M' X Y
inst✝ : MulActionHomClass F X X Y
f : F
m : M'
x : X
⊢ m • f (x • 1) = id m • f x
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝ : Monoid M
f : M →ₑ[id] M
m : M
⊢ m • f 1 = f m

Tactic:
← map_smul,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝ : Monoid M
f : M →ₑ[id] M
m : M
⊢ f (m • 1) = f m
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝ : Monoid M
f g : M →ₑ[id] M
⊢ (f • g) 1 = g 1 • f 1

Tactic:
← map_smul,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝ : Monoid M
f g : M →ₑ[id] M
⊢ (f • g) 1 = f (g 1 • 1)
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: R : Type u_10
inst✝³ : Semiring R
S : Type u_11
inst✝² : Semiring S
N' : Type u_13
inst✝¹ : AddMonoid N'
inst✝ : DistribMulAction S N'
σ : R →* S
f g : R →ₑ+[σ] N'
h : f 1 = g 1
x : R
⊢ f x = g x

Tactic:
rw [← mul_one x, ← smul_eq_mul, f.map_smulₑ, g.map_smulₑ, h]

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 : Set (Submodule R M)
t : R
m : M
h : m ∈ ⨆ a, ↑a
⊢ t • m ∈ ⨆ a, ↑a

Tactic:
induction h using AddSubmonoid.iSup_induction' with
        | mem p x hx =>
          obtain ⟨-, ⟨p : Submodule R M, hp : p ∈ s, rfl⟩⟩ := p
          suffices p.toAddSubmonoid ≤ ⨆ q : toAddSubmonoid '' s, (q : AddSubmonoid M) by
            exact this (smul_mem p t hx)
          apply le_sSup
          rw [Subtype.range_coe_subtype]
          exact ⟨p, hp, rfl⟩
        | zero => simpa only [smul_zero] using zero_mem _
        | add _ _ _ _ mx my => revert mx my; simp_rw [smul_add]; exact add_mem

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

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
⊢ closure ↑(AddSubmonoid.closure s) = closure s

Tactic:
by
  ext x
  refine ⟨fun hx => ?_, fun hx => closure_mono AddSubmonoid.subset_closure hx⟩
  rintro - ⟨H, rfl⟩
  rintro - ⟨J, rfl⟩
  refine (AddSubmonoid.mem_closure.mp (mem_closure_iff.mp hx)) H.toAddSubmonoid fun y hy => ?_
  refine (Subsemigroup.mem_closure.mp hy) H.toSubsemigroup fun z hz => ?_
  exact (AddSubmonoid.mem_closure.mp hz) H.toAddSubmonoid fun w hw => J hw

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

Goal state before:
pp: R : Type u
S : Type v
T : Type u_1
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : NonUnitalNonAssocRing S
inst✝ : NonUnitalNonAssocRing T
g : S →ₙ+* T
f : R →ₙ+* S
⊢ NonUnitalSubring.map g f.range = (g.comp f).range

Tactic:
simpa only [range_eq_map] using (⊤ : NonUnitalSubring R).map_map g f

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₗ[R] B
hf : f 1 = 1
r : R
h : Invertible ((algebraMap R A) r)
⊢ r • f ⅟((algebraMap R A) r) = 1

Tactic:
← map_smul,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₗ[R] B
hf : f 1 = 1
r : R
h : Invertible ((algebraMap R A) r)
⊢ f (r • ⅟((algebraMap R A) r)) = 1
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
b : F →ₗ[F] E
hb : Surjective ⇑b
x y z : F
hz : b z = 1
hy : x • z • b y = x • z • (b 1 * b 1)
⊢ (algebraMap F E) (x * y) = b x

Tactic:
← map_smul,

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
b : F →ₗ[F] E
hb : Surjective ⇑b
x y z : F
hz : b z = 1
hy : x • b (z • y) = x • z • (b 1 * b 1)
⊢ (algebraMap F E) (x * y) = b x
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
b : F →ₗ[F] E
hb : Surjective ⇑b
x y z : F
hz : b z = 1
hy : x • y • 1 = x • b 1
⊢ (algebraMap F E) (x * y) = b x

Tactic:
← map_smul,

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
b : F →ₗ[F] E
hb : Surjective ⇑b
x y z : F
hz : b z = 1
hy : x • y • 1 = b (x • 1)
⊢ (algebraMap F E) (x * y) = b x
Module: Mathlib.Algebra.Prime.Defs

Goal state before:
pp: case zero
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
h : p ∣ 1
⊢ p ∣ a

Tactic:
have := isUnit_of_dvd_one h

Goal state after:
case zero
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
h : p ∣ 1
this : IsUnit p
⊢ p ∣ a
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
⊢ Irreducible (y * ↑u) ↔ Irreducible y

Tactic:
by
  simp only [irreducible_iff, Units.isUnit_mul_units, and_congr_right_iff]
  refine fun _ => ⟨fun h A B HAB => ?_, fun h A B HAB => ?_⟩
  · rw [← u.isUnit_mul_units B]
    apply h
    rw [← mul_assoc, ← HAB]
  · rw [← u⁻¹.isUnit_mul_units B]
    apply h
    rw [← mul_assoc, ← HAB, Units.mul_inv_cancel_right]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
q r : M
u : Mˣ
h' : q * ↑u ~ᵤ q
hp : q * ↑u ≠ 0
x : M
hx : ¬IsUnit x ∧ r = q * ↑u * x
hq : q ≠ 0
⊢ r = q * (x * ↑u)

Tactic:
rw [mul_comm x, ← mul_assoc, ← hx.2]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
e : R ≃ₗ[R] A
x : A
⊢ (algebraMap R A) (e.symm 1) * e.symm (e 1 * x) • e 1 = x

Tactic:
← map_smul,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
e : R ≃ₗ[R] A
x : A
⊢ (algebraMap R A) (e.symm 1) * e (e.symm (e 1 * x) • 1) = x
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
e : R ≃ₗ[R] A
x : A
⊢ e.symm 1 • e 1 * x = x

Tactic:
← map_smul,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
e : R ≃ₗ[R] A
x : A
⊢ e (e.symm 1 • 1) * x = x
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_10
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : ↥O →ₗ[R] M'
N : Submodule R M
x : M'
y : M
yO : y ∈ O
yN : y ∈ N
h : ϕ ⟨y, yO⟩ = x
⊢ ∃ y, O.subtype y ∈ N ∧ ϕ y = x

Tactic:
exact ⟨⟨y, yO⟩, yN, h⟩

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝ : Preorder α
⊢ IsStronglyCoatomic αᵒᵈ ↔ IsStronglyAtomic α

Tactic:
rw [← isStronglyAtomic_dual_iff_is_stronglyCoatomic]; rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
f : R →ₗ[R] ↥s
hf : Surjective ⇑f
x : M
hx : x ∈ s
r : R
eq : f r = ⟨x, hx⟩
⊢ ↑(r • f 1) = x

Tactic:
← map_smul,

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
f : R →ₗ[R] ↥s
hf : Surjective ⇑f
x : M
hx : x ∈ s
r : R
eq : f r = ⟨x, hx⟩
⊢ ↑(f (r • 1)) = x
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
a b c : R
⊢ a • x + b • y + c • z = a • x + (b • y + c • z)

Tactic:
by rw [add_assoc]

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hf : ∀ i ∈ t, f i ∈ s
⊢ ⨆ i ∈ t, f i ∈ s

Tactic:
by
  rw [← sSup_image]
  exact hs.sSup_mem (ht.image _) hbot (by simpa)

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

Goal state before:
pp: R : Type u_8
A : Type u_9
inst✝⁴ : Semiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x : A
h : ∀ y ∈ s, Commute y x
y : A
hy : y ∈ span R s
⊢ Commute y x

Tactic:
induction hy using span_induction with

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
i : ι
a✝ : i ∈ {i | t i ≠ ⊥}
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
this : t j ≤ ⨆ k, ⨆ (_ : k ≠ i), t k
⊢ t j = ⊥

Tactic:
replace ht := (ht i).mono_right this
    rwa [h, disjoint_self] at ht

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

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
h : EqOn f g s
x : α
⊢ s.mulIndicator f x = s.mulIndicator g x

Tactic:
simp only [mulIndicator]

Goal state after:
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
h : EqOn f g s
x : α
⊢ (if x ∈ s then f x else 1) = if x ∈ s then g x else 1
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
x : α
⊢ s.mulIndicator (t.mulIndicator f) x = (s ∩ t).mulIndicator f x

Tactic:
simp only [mulIndicator]

Goal state after:
α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
x : α
⊢ (if x ∈ s then if x ∈ t then f x else 1 else 1) = if x ∈ s ∩ t then f x else 1
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : One M
inst✝ : One N
s : Set α
f : α → M
g : M → N
hg : g 1 = 1
x✝ : α
⊢ s.mulIndicator (g ∘ f) x✝ = (g ∘ s.mulIndicator f) x✝

Tactic:
simp only [mulIndicator]

Goal state after:
α : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : One M
inst✝ : One N
s : Set α
f : α → M
g : M → N
hg : g 1 = 1
x✝ : α
⊢ (if x✝ ∈ s then (g ∘ f) x✝ else 1) = (g ∘ s.mulIndicator f) x✝
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
contra : s.Infinite
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
⊢ ∃ x ∈ s, x ≠ ⊥ ∧ x ∉ t

Tactic:
have : (s \ (insert ⊥ t : Finset α)).Infinite := contra.sdiff (Finset.finite_toSet _)

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
contra : s.Infinite
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
this : (s \ ↑(insert ⊥ t)).Infinite
⊢ ∃ x ∈ s, x ≠ ⊥ ∧ x ∉ t
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
t : Set A
k : S
hks : k ∈ span R s
x : A
hx : x ∈ t
c₁ c₂ : S
x✝¹ : c₁ ∈ span R s
x✝ : c₂ ∈ span R s
ih₁ : c₁ • x ∈ span R (s • t)
ih₂ : c₂ • x ∈ span R (s • t)
⊢ (c₁ + c₂) • x ∈ span R (s • t)

Tactic:
by rw [add_smul]; exact add_mem ih₁ ih₂

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

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha : a ∈ s → r (f a) (g a)
⊢ r (s.mulIndicator f a) (s.mulIndicator g a)

Tactic:
simp only [mulIndicator]

Goal state after:
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha : a ∈ s → r (f a) (g a)
⊢ r (if a ∈ s then f a else 1) (if a ∈ s then g a else 1)
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : ¬Nonempty η
⊢ sSupIndep (⋃ i, s i)

Tactic:
· rintro a ⟨_, ⟨i, _⟩, _⟩
    exfalso
    exact hη ⟨i⟩

Goal state after:
Module: Mathlib.Data.Multiset.Sections

Goal state before:
pp: α : Type u_1
a : List α
l : List (List α)
⊢ (↑(↑a :: List.map (fun l ↦ ↑l) l)).Sections =
    ↑(List.map (fun l ↦ ↑l) (List.flatMap (fun s ↦ List.map (fun a ↦ a :: s) a) l.sections))

Tactic:
← cons_coe,

Goal state after:
α : Type u_1
a : List α
l : List (List α)
⊢ (↑a ::ₘ ↑(List.map (fun l ↦ ↑l) l)).Sections =
    ↑(List.map (fun l ↦ ↑l) (List.flatMap (fun s ↦ List.map (fun a ↦ a :: s) a) l.sections))
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
s : Set α
f g : α → M
x✝ : α
⊢ s.mulIndicator (fun a ↦ f a * g a) x✝ = s.mulIndicator f x✝ * s.mulIndicator g x✝

Tactic:
simp only [mulIndicator]

Goal state after:
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
s : Set α
f g : α → M
x✝ : α
⊢ (if x✝ ∈ s then f x✝ * g x✝ else 1) = (if x✝ ∈ s then f x✝ else 1) * if x✝ ∈ s then g x✝ else 1
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
he : Injective e
a b : α →₀ M
h : ∀ (a_1 : α), (mapRange e he₀ a) a_1 = (mapRange e he₀ b) a_1
⊢ ∀ (a_1 : α), a a_1 = b a_1

Tactic:
simpa only [mapRange_apply, he.eq_iff] using h

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : f.ker = ⊥
p p' : Submodule R M
⊢ map f p ≤ map f p' ↔ p ≤ p'

Tactic:
by
  rw [LinearMap.map_le_map_iff, hf, sup_bot_eq]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : Module.End R R
⊢ f 1 • f 1 = f 1 ↔ IsIdempotentElem f

Tactic:
← map_smul,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : Module.End R R
⊢ f (f 1 • 1) = f 1 ↔ IsIdempotentElem f
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
b b' : M
hb : b ≠ 0
hb' : b' ≠ 0
i j : α
⊢ Disjoint (single i b).support (single j b').support ↔ i ≠ j

Tactic:
rw [support_single _ hb, support_single _ hb', disjoint_singleton]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f✝ : α →₀ M
a✝ : α
b✝ : M
i✝ : α
f : α →₀ M
a : α
b : M
i : α
⊢ (i ∈ if b = 0 then f.support.erase a else insert a f.support) ↔ Function.update (⇑f) a b i ≠ 0

Tactic:
classical
    grind

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

Goal state before:
pp: case neg
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∉ ⋃ i, s i
⊢ (⋃ i, s i).mulIndicator (⨆ i, f i) a ≤ (⨆ i, (s i).mulIndicator (f i)) a

Tactic:
· rw [mulIndicator_of_notMem ha, ← h1]
    exact bot_le

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : Preorder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f g : ι → R
s : Finset ι
h0 : ∀ i ∈ s, 0 ≤ f i
h1 : ∀ i ∈ s, f i ≤ g i
⊢ ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i

Tactic:
induction s using Finset.cons_induction with
  | empty => simp
  | cons a s has ih =>
    simp only [prod_cons, forall_mem_cons] at h0 h1 ⊢
    have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
    gcongr
    exacts [prod_nonneg h0.2, h0.1.trans h1.1, h1.1, ih h0.2 h1.2]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : Preorder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ t, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → f i ≤ 1
this : MulPosMono R
⊢ ∏ i ∈ t, f i ≤ ∏ i ∈ s, f i

Tactic:
calc
    ∏ i ∈ t, f i = ∏ i ∈ t \ s ∪ s, f i := by rw [sdiff_union_of_subset h]
    _ = (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i := prod_union sdiff_disjoint
    _ ≤ ∏ i ∈ s, f i :=
      mul_le_of_le_one_left (prod_nonneg (by grind)) (prod_le_one (by grind) (by grind))

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

Goal state before:
pp: case cons
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
⊢ (map f (a :: s)).prod ≤ (map g (a :: s)).prod

Tactic:
| cons a s hind =>

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

Goal state before:
pp: case cons
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
a : R
s : List R
hind : (∀ (a : R), a ∈ s → 0 < a) → 0 < s.prod
h : ∀ (a_1 : R), a_1 ∈ a :: s → 0 < a_1
⊢ 0 < (a :: s).prod

Tactic:
| cons a s hind =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : AddZeroClass α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
⊢ (erase i f).sum g + (single i a).sum g + g i (f i) = (f.update i (f i)).sum g + g i a

Tactic:
rw [update_eq_erase_add_single, sum_add_index' hg hgg, add_assoc, add_assoc]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : AddZeroClass α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
⊢ (erase i f).sum g + ((single i a).sum g + g i (f i)) = (erase i f).sum g + ((single i (f i)).sum g + g i a)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case refine_2
M : Type u_5
inst✝ : AddCommMonoid M
l : ℕ →₀ M
x✝ : ℕ
⊢ x✝ ∈ ↑(erase 0 l).support → x✝ ∈ Set.range fun x ↦ x + 1

Tactic:
· simp_all [Nat.pos_iff_ne_zero]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
f : α → β
s : Finset α
t : Finset β
Hf : ∀ a ∈ s, f a ∈ t
n : ℕ
hn : ∀ b ∈ t, #({a ∈ s | f a = b}) ≤ n
⊢ ∑ _b ∈ t, n = n * #t

Tactic:
simp [mul_comm]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
f : α → β
s : Finset α
t : Finset β
Hf : ∀ a ∈ s, f a ∈ t
n : ℕ
hn : ∀ b ∈ t, n ≤ #({a ∈ s | f a = b})
⊢ n * #t = ∑ _a ∈ t, n

Tactic:
simp [mul_comm]

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

Goal state before:
pp: α : Type u_1
M : Type u_3
G : Type u_5
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
g : G
f : α →₀ M
a : α
⊢ (g • f) a = f (g⁻¹ • a)

Tactic:
conv_lhs => rw [← smul_inv_smul g a]

Goal state after:
α : Type u_1
M : Type u_3
G : Type u_5
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
g : G
f : α →₀ M
a : α
⊢ (g • f) (g • g⁻¹ • a) = f (g⁻¹ • a)