harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Antidiag/Pi.lean
lemma nsmul_piAntidiag_univ [Fintype ι] (m : ℕ) {n : ℕ} (hn : n ≠ 0) :
    @SMul.smul _ _ Finset.smulFinset n (piAntidiag univ m) =
      (piAntidiag univ (n * m)).filter fun f : ι → ℕ ↦ ∀ i, n ∣ f i

Proof state:
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m n : ℕ
hn : n ≠ 0
⊢ SMul.smul n (univ.piAntidiag m) = filter (fun f => ∀ (i : ι), n ∣ f i) (univ.piAntidiag (n * m))

Tactic:
simpa using nsmul_piAntidiag (univ : Finset ι) m hn

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem sub_one_mul_padicValNat_factorial [hp : Fact p.Prime] (n : ℕ) :
    (p - 1) * padicValNat p (n !) = n - (p.digits n).sum

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (p - 1) * ∑ i ∈ Finset.Ico (0 + 1) (log p n).succ.succ, n / p ^ i = n - (p.digits n).sum

Tactic:
rw [Nat.succ_eq_add_one, ← Finset.sum_Ico_add' _ 0 _ 1,
  Ico_zero_eq_range, ← sub_one_mul_sum_log_div_pow_eq_sub_sum_digits, Nat.succ_eq_add_one]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (p - 1) * ∑ i ∈ Finset.Ico 1 (log p n).succ.succ, n / p ^ i = n - (p.digits n).sum

Tactic:
nth_rw 2 [← zero_add 1]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (p - 1) * ∑ i ∈ Finset.Ico (0 + 1) (log p n).succ.succ, n / p ^ i = n - (p.digits n).sum

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (p - 1) * padicValNat p n ! = n - (p.digits n).sum

Tactic:
rw [padicValNat_factorial <| lt_succ_of_lt <| lt.base (log p n)]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (p - 1) * ∑ i ∈ Finset.Ico 1 (log p n).succ.succ, n / p ^ i = n - (p.digits n).sum
-- Mathlib/Tactic/NormNum/Pow.lean
theorem isNat_zpow_neg {α : Type*} [DivisionSemiring α] {a : α} {b : ℤ} {nb ne : ℕ}
    (pb : IsInt b (Int.negOfNat nb)) (pe' : IsNat (a ^ nb)⁻¹ ne) :
    IsNat (a ^ b) ne

Proof state:
α : Type u_1
inst✝ : DivisionSemiring α
a : α
b : ℤ
nb ne : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsNat (a ^ nb)⁻¹ ne
⊢ IsNat (a ^ b) ne

Tactic:
rwa [pb.out, Int.cast_negOfNat, zpow_neg, zpow_natCast]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem log_abs (x : ℝ) : log |x| = log x

Proof state:
case neg
x : ℝ
h : ¬x = 0
⊢ log |x| = log x

Tactic:
rw [← exp_eq_exp, exp_log_eq_abs h, exp_log_eq_abs (abs_pos.2 h).ne', abs_abs]

Result:
no goals

Proof state:
case pos
x : ℝ
h : x = 0
⊢ log |x| = log x

Tactic:
simp [h]

Result:
no goals

Proof state:
x : ℝ
⊢ log |x| = log x

Tactic:
by_cases h : x = 0

Result:
case pos
x : ℝ
h : x = 0
⊢ log |x| = log x

case neg
x : ℝ
h : ¬x = 0
⊢ log |x| = log x
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem inf_congr {f g : β → α} (hs : s₁ = s₂) (hfg : ∀ a ∈ s₂, f a = g a) :
    s₁.inf f = s₂.inf g

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
s₁ s₂ : Finset β
f g : β → α
hs : s₁ = s₂
hfg : ∀ a ∈ s₂, f a = g a
⊢ s₁.inf f = s₂.inf g

Tactic:
subst hs

Result:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
s₁ : Finset β
f g : β → α
hfg : ∀ a ∈ s₁, f a = g a
⊢ s₁.inf f = s₁.inf g

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
s₁ : Finset β
f g : β → α
hfg : ∀ a ∈ s₁, f a = g a
⊢ s₁.inf f = s₁.inf g

Tactic:
exact Finset.fold_congr hfg

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_set_coe_eq_finprod_mem (s : Set α) : ∏ᶠ j : s, f j = ∏ᶠ i ∈ s, f i

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
⊢ Injective Subtype.val

Tactic:
exact Subtype.coe_injective

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
⊢ ∏ᶠ (j : ↑s), f ↑j = ∏ᶠ (i : α) (_ : i ∈ s), f i

Tactic:
rw [← finprod_mem_range, Subtype.range_coe]

Result:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
⊢ Injective Subtype.val
-- Mathlib/Logic/Denumerable.lean
theorem prod_nat_ofNat : ofNat (ℕ × ℕ) = unpair

Proof state:
case h
x✝ : ℕ
⊢ ofNat (ℕ × ℕ) x✝ = unpair x✝

Tactic:
simp

Result:
no goals

Proof state:
⊢ ofNat (ℕ × ℕ) = unpair

Tactic:
funext

Result:
case h
x✝ : ℕ
⊢ ofNat (ℕ × ℕ) x✝ = unpair x✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem toArray_pmap {l : Vector α n} {P : α → Prop} {f : ∀ a, P a → β} {H : ∀ a ∈ l, P a} :
    (l.pmap f H).toArray = l.toArray.pmap f (fun a m => H a (by simpa using m))

Proof state:
α : Type ?u.4741
n : Nat
β : Type ?u.4793
l : Vector α n
P : α → Prop
f : (a : α) → P a → β
H : ∀ (a : α), a ∈ l → P a
a : α
m : a ∈ l.toArray
⊢ a ∈ l

Tactic:
simpa using m

Result:
no goals

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
P : α → Prop
f : (a : α) → P a → β
H : ∀ (a : α), a ∈ l → P a
⊢ (pmap f l H).toArray = Array.pmap f l.toArray ⋯

Tactic:
simp [pmap]

Result:
no goals
-- Mathlib/Data/Finset/Sort.lean
theorem listMap_orderEmbOfFin_finRange (s : Finset α) {k : ℕ} (h : s.card = k) :
    (List.finRange k).map (s.orderEmbOfFin h) = s.sort (· ≤ ·)

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
⊢ k = (sort (fun x1 x2 => x1 ≤ x2) s).length

Tactic:
simp [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem State.Inv_nil : State.Inv ([] : CNF (CNFVar aig))

Proof state:
aig : AIG Nat
⊢ Inv []

Tactic:
simp [State.Inv]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {k a : α}
    {v : β} : get! (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then v else get! m a

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.WF
k a : α
v : β
⊢ get! (m.insertIfNew k v) a = if (k == a) = true ∧ m.contains k = false then v else get! m a

Tactic:
simp_to_raw using Raw₀.Const.get!_insertIfNew

Result:
no goals

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.WF
k a : α
v : β
⊢ get! (m.insertIfNew k v) a = if (k == a) = true ∧ ¬k ∈ m then v else get! m a

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.WF
k a : α
v : β
⊢ get! (m.insertIfNew k v) a = if (k == a) = true ∧ m.contains k = false then v else get! m a
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem norm_div_sin_oangle_sub_left_of_oangle_eq_pi_div_two {x y : V}
    (h : o.oangle x y = ↑(π / 2)) : ‖y‖ / Real.Angle.sin (o.oangle (x - y) x) = ‖x - y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ‖y‖ / ((-o).oangle x (x - y)).sin = ‖x - y‖

Tactic:
exact (-o).norm_div_sin_oangle_sub_right_of_oangle_eq_pi_div_two h

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ ‖y‖ / (o.oangle (x - y) x).sin = ‖x - y‖

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ‖y‖ / ((-o).oangle x (x - y)).sin = ‖x - y‖
-- Mathlib/Algebra/GeomSum.lean
theorem geom_sum_mul_of_le_one [CommSemiring α] [PartialOrder α] [AddLeftReflectLE α]
    [AddLeftMono α] [ExistsAddOfLE α] [Sub α] [OrderedSub α] {x : α} (hx : x ≤ 1) (n : ℕ) :
    (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n

Proof state:
α : Type u
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : AddLeftReflectLE α
inst✝³ : AddLeftMono α
inst✝² : ExistsAddOfLE α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x : α
hx : x ≤ 1
n : ℕ
⊢ (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n

Tactic:
simpa using geom_sum₂_mul_of_le hx n

Result:
no goals
-- Mathlib/RingTheory/Localization/Integer.lean
theorem exists_integer_multiple (a : S) : ∃ b : M, IsInteger R ((b : R) • a)

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a : S
⊢ ∃ b, IsInteger R (a * (algebraMap R S) ↑b)

Tactic:
apply exists_integer_multiple'

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a : S
⊢ ∃ b, IsInteger R (↑b • a)

Tactic:
simp_rw [Algebra.smul_def, mul_comm _ a]

Result:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a : S
⊢ ∃ b, IsInteger R (a * (algebraMap R S) ↑b)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Impl.lean
theorem flatMap_eq_flatMapTR : @List.flatMap = @flatMapTR

Proof state:
α : Type u_2
β : Type u_1
f : α → List β
as : List α
acc : Array β
⊢ flatMapTR.go f [] acc = acc.toList ++ flatMap f []

Tactic:
simp [flatMapTR.go, flatMap]

Result:
no goals

Proof state:
⊢ @flatMap = @flatMapTR

Tactic:
funext α β f as

Result:
case h.h.h.h
α : Type u_2
β : Type u_1
f : α → List β
as : List α
⊢ flatMap f as = flatMapTR f as

Proof state:
case h.h.h.h
α : Type u_2
β : Type u_1
f : α → List β
as : List α
⊢ flatMap f as = flatMapTR f as

Tactic:
exact (go as #[]).symm

Result:
no goals

Proof state:
α : Type u_2
β : Type u_1
f : α → List β
as : List α
x : α
xs : List α
acc : Array β
⊢ flatMapTR.go f (x :: xs) acc = acc.toList ++ flatMap f (x :: xs)

Tactic:
simp [flatMapTR.go, flatMap, go xs]

Result:
no goals
-- Mathlib/Data/Matrix/ColumnRowPartitioned.lean
@[simp]
lemma fromCols_zero : fromCols (0 : Matrix m n₁ R) (0 : Matrix m n₂ R) = 0

Proof state:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝ : Semiring R
⊢ fromCols 0 0 = 0

Tactic:
ext _ (_ | _) <;> simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffEdist_self_closure : hausdorffEdist s (closure s) = 0

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
⊢ hausdorffEdist s (closure s) = 0

Tactic:
rw [hausdorffEdist_zero_iff_closure_eq_closure, closure_closure]

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem support_curry [DecidableEq α] (f : α × β →₀ M) :
    f.curry.support ⊆ f.support.image Prod.fst

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
f : α × β →₀ M
⊢ (f.support.biUnion fun a => (single a.1 (single a.2 (f a))).support) ⊆ f.support.biUnion fun a => {a.1}

Tactic:
exact Finset.biUnion_mono fun a _ => support_single_subset

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
f : α × β →₀ M
⊢ f.curry.support ⊆ f.support.biUnion fun a => {a.1}

Tactic:
refine Finset.Subset.trans support_sum ?_

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
f : α × β →₀ M
⊢ (f.support.biUnion fun a => (single a.1 (single a.2 (f a))).support) ⊆ f.support.biUnion fun a => {a.1}

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
f : α × β →₀ M
⊢ f.curry.support ⊆ image Prod.fst f.support

Tactic:
rw [← Finset.biUnion_singleton]

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
f : α × β →₀ M
⊢ f.curry.support ⊆ f.support.biUnion fun a => {a.1}
-- Mathlib/CategoryTheory/Triangulated/Basic.lean
@[reassoc (attr := simp)]
lemma _root_.CategoryTheory.Iso.hom_inv_id_triangle_hom₁ {A B : Triangle C} (e : A ≅ B) :
    e.hom.hom₁ ≫ e.inv.hom₁ = 𝟙 _

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
e : A ≅ B
⊢ e.hom.hom₁ ≫ e.inv.hom₁ = 𝟙 A.obj₁

Tactic:
rw [← comp_hom₁, e.hom_inv_id, id_hom₁]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem multiset_sum_sum_index [AddCommMonoid M] [AddCommMonoid N] (f : Multiset (α →₀ M))
    (h : α → M → N) (h₀ : ∀ a, h a 0 = 0)
    (h₁ : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) :
    f.sum.sum h = (f.map fun g : α →₀ M => g.sum h).sum :=
  Multiset.induction_on f rfl fun a s ih => by
    rw [Multiset.sum_cons, Multiset.map_cons, Multiset.sum_cons, sum_add_index' h₀ h₁, ih]

Proof state:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : Multiset (α →₀ M)
h : α → M → N
h₀ : ∀ (a : α), h a 0 = 0
h₁ : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂
a : α →₀ M
s : Multiset (α →₀ M)
ih : s.sum.sum h = (Multiset.map (fun g => g.sum h) s).sum
⊢ (a ::ₘ s).sum.sum h = (Multiset.map (fun g => g.sum h) (a ::ₘ s)).sum

Tactic:
rw [Multiset.sum_cons, Multiset.map_cons, Multiset.sum_cons, sum_add_index' h₀ h₁, ih]

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem im_sq : a.im ^ 2 = -normSq a.im

Proof state:
R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ a.im ^ 2 = -↑(normSq a.im)

Tactic:
simp_rw [sq, ← star_mul_self, im_star, neg_mul, neg_neg]

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject/Monoidal.lean
@[simp]
lemma tensor_id (X Y : GradedObject I C) [HasTensor X Y] :
    tensorHom (𝟙 X) (𝟙 Y) = 𝟙 _

Proof state:
I : Type u
inst✝³ : AddMonoid I
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : MonoidalCategory C
X Y : GradedObject I C
inst✝ : X.HasTensor Y
⊢ 𝟙 ((((mapBifunctor (curriedTensor C) I I).obj X).obj Y).mapObj fun x => x.1 + x.2) = 𝟙 (tensorObj X Y)

Tactic:
rfl

Result:
no goals

Proof state:
I : Type u
inst✝³ : AddMonoid I
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : MonoidalCategory C
X Y : GradedObject I C
inst✝ : X.HasTensor Y
⊢ (mapMap
      (((mapBifunctor (curriedTensor C) I I).map (𝟙 X)).app Y ≫ ((mapBifunctor (curriedTensor C) I I).obj X).map (𝟙 Y))
      fun x => x.1 + x.2) =
    𝟙 (tensorObj X Y)

Tactic:
simp only [Functor.map_id, NatTrans.id_app, comp_id, mapMap_id]

Result:
I : Type u
inst✝³ : AddMonoid I
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : MonoidalCategory C
X Y : GradedObject I C
inst✝ : X.HasTensor Y
⊢ 𝟙 ((((mapBifunctor (curriedTensor C) I I).obj X).obj Y).mapObj fun x => x.1 + x.2) = 𝟙 (tensorObj X Y)

Proof state:
I : Type u
inst✝³ : AddMonoid I
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : MonoidalCategory C
X Y : GradedObject I C
inst✝ : X.HasTensor Y
⊢ tensorHom (𝟙 X) (𝟙 Y) = 𝟙 (tensorObj X Y)

Tactic:
dsimp [tensorHom, mapBifunctorMapMap]

Result:
I : Type u
inst✝³ : AddMonoid I
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : MonoidalCategory C
X Y : GradedObject I C
inst✝ : X.HasTensor Y
⊢ (mapMap
      (((mapBifunctor (curriedTensor C) I I).map (𝟙 X)).app Y ≫ ((mapBifunctor (curriedTensor C) I I).obj X).map (𝟙 Y))
      fun x => x.1 + x.2) =
    𝟙 (tensorObj X Y)
-- Mathlib/Data/Sym/Sym2.lean
theorem other_spec {a : α} {z : Sym2 α} (h : a ∈ z) : s(a, Mem.other h) = z

Proof state:
α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
⊢ s(a, Mem.other h) = z

Tactic:
erw [← Classical.choose_spec h]

Result:
no goals
-- Mathlib/Order/BoundedOrder/Lattice.lean
theorem sup_eq_bot_iff : a ⊔ b = ⊥ ↔ a = ⊥ ∧ b = ⊥

Proof state:
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a b : α
⊢ a ≤ ⊥ ∧ b ≤ ⊥ ↔ a = ⊥ ∧ b = ⊥

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a b : α
⊢ a ⊔ b = ⊥ ↔ a = ⊥ ∧ b = ⊥

Tactic:
rw [eq_bot_iff, sup_le_iff]

Result:
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a b : α
⊢ a ≤ ⊥ ∧ b ≤ ⊥ ↔ a = ⊥ ∧ b = ⊥
-- Mathlib/Algebra/Group/Units/Defs.lean
theorem inv_mul_cancel : IsUnit a → a⁻¹ * a = 1

Proof state:
α : Type u
inst✝ : DivisionMonoid α
a : α
⊢ IsUnit a → a⁻¹ * a = 1

Tactic:
rintro ⟨u, rfl⟩

Result:
case intro
α : Type u
inst✝ : DivisionMonoid α
u : αˣ
⊢ (↑u)⁻¹ * ↑u = 1

Proof state:
case intro
α : Type u
inst✝ : DivisionMonoid α
u : αˣ
⊢ (↑u)⁻¹ * ↑u = 1

Tactic:
rw [← Units.val_inv_eq_inv_val, Units.inv_mul]

Result:
no goals
-- Mathlib/Combinatorics/Young/SemistandardTableau.lean
theorem row_weak_of_le {μ : YoungDiagram} (T : SemistandardYoungTableau μ) {i j1 j2 : ℕ}
    (hj : j1 ≤ j2) (cell : (i, j2) ∈ μ) : T i j1 ≤ T i j2

Proof state:
μ : YoungDiagram
T : SemistandardYoungTableau μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
⊢ T i j1 ≤ T i j2

Tactic:
rcases eq_or_lt_of_le hj with h | h

Result:
case inl
μ : YoungDiagram
T : SemistandardYoungTableau μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
h : j1 = j2
⊢ T i j1 ≤ T i j2

case inr
μ : YoungDiagram
T : SemistandardYoungTableau μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
h : j1 < j2
⊢ T i j1 ≤ T i j2

Proof state:
case inl
μ : YoungDiagram
T : SemistandardYoungTableau μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
h : j1 = j2
⊢ T i j1 ≤ T i j2

Tactic:
rw [h]

Result:
no goals

Proof state:
case inr
μ : YoungDiagram
T : SemistandardYoungTableau μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
h : j1 < j2
⊢ T i j1 ≤ T i j2

Tactic:
exact T.row_weak h cell

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem norm_Lp_toLp_restrict_le (s : Set X) (f : Lp E p μ) :
    ‖((Lp.memLp f).restrict s).toLp f‖ ≤ ‖f‖

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
s : Set X
f : ↥(Lp E p μ)
⊢ eLpNorm (↑↑f) p (μ.restrict s) ≤ eLpNorm (↑↑f) p μ

Tactic:
exact eLpNorm_mono_measure _ Measure.restrict_le_self

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
s : Set X
f : ↥(Lp E p μ)
⊢ (eLpNorm (↑↑f) p (μ.restrict s)).toReal ≤ (eLpNorm (↑↑f) p μ).toReal

Tactic:
refine ENNReal.toReal_mono (Lp.eLpNorm_ne_top _) ?_

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
s : Set X
f : ↥(Lp E p μ)
⊢ eLpNorm (↑↑f) p (μ.restrict s) ≤ eLpNorm (↑↑f) p μ

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
s : Set X
f : ↥(Lp E p μ)
⊢ ‖MemLp.toLp ↑↑f ⋯‖ ≤ ‖f‖

Tactic:
rw [Lp.norm_def, Lp.norm_def, eLpNorm_congr_ae (MemLp.coeFn_toLp _)]

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
s : Set X
f : ↥(Lp E p μ)
⊢ (eLpNorm (↑↑f) p (μ.restrict s)).toReal ≤ (eLpNorm (↑↑f) p μ).toReal
-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem eraseLead_natDegree_le (f : R[X]) : (eraseLead f).natDegree ≤ f.natDegree - 1

Proof state:
case inl
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead.natDegree < f.natDegree
⊢ f.eraseLead.natDegree ≤ f.natDegree - 1

Tactic:
exact Nat.le_sub_one_of_lt h

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.eraseLead.natDegree ≤ f.natDegree - 1

Tactic:
rcases f.eraseLead_natDegree_lt_or_eraseLead_eq_zero with (h | h)

Result:
case inl
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead.natDegree < f.natDegree
⊢ f.eraseLead.natDegree ≤ f.natDegree - 1

case inr
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead = 0
⊢ f.eraseLead.natDegree ≤ f.natDegree - 1

Proof state:
case inr
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead = 0
⊢ f.eraseLead.natDegree ≤ f.natDegree - 1

Tactic:
simp only [h, natDegree_zero, zero_le]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Rename.lean
theorem eval₂_rename_prod_mk (g : σ × τ → S) (i : σ) (p : MvPolynomial τ R) :
    (rename (Prod.mk i) p).eval₂ f g = eval₂ f (fun j => g (i, j)) p

Proof state:
case h_X
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ × τ → S
i : σ
p p✝ : MvPolynomial τ R
n✝ : τ
a✝ : eval₂ f g ((rename (Prod.mk i)) p✝) = eval₂ f (fun j => g (i, j)) p✝
⊢ eval₂ f g ((rename (Prod.mk i)) (p✝ * X n✝)) = eval₂ f (fun j => g (i, j)) (p✝ * X n✝)

Tactic:
simp [*]

Result:
no goals

Proof state:
case h_X
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ × τ → S
i : σ
p : MvPolynomial τ R
⊢ ∀ (p : MvPolynomial τ R) (n : τ),
    eval₂ f g ((rename (Prod.mk i)) p) = eval₂ f (fun j => g (i, j)) p →
      eval₂ f g ((rename (Prod.mk i)) (p * X n)) = eval₂ f (fun j => g (i, j)) (p * X n)

Tactic:
intros

Result:
case h_X
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ × τ → S
i : σ
p p✝ : MvPolynomial τ R
n✝ : τ
a✝ : eval₂ f g ((rename (Prod.mk i)) p✝) = eval₂ f (fun j => g (i, j)) p✝
⊢ eval₂ f g ((rename (Prod.mk i)) (p✝ * X n✝)) = eval₂ f (fun j => g (i, j)) (p✝ * X n✝)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem any_dropWhile {l : List α} :
    (l.dropWhile p).any (fun x => !p x) = !l.all p

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ ((dropWhile p l).any fun x => !p x) = !l.all p

Tactic:
induction l with
| nil => rfl
| cons h t ih => by_cases p h <;> simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
h : α
t : List α
ih : ((dropWhile p t).any fun x => !p x) = !t.all p
⊢ ((dropWhile p (h :: t)).any fun x => !p x) = !(h :: t).all p

Tactic:
by_cases p h <;> simp_all

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Bool
⊢ ((dropWhile p []).any fun x => !p x) = ![].all p

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/ContinuousAffineEquiv.lean
theorem coe_injective : Function.Injective ((↑) : (P₁ ≃ᵃL[k] P₂) → P₁ ≃ᵃ[k] P₂)

Proof state:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module k V₁
inst✝⁵ : AddTorsor V₁ P₁
inst✝⁴ : TopologicalSpace P₁
inst✝³ : AddCommGroup V₂
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₂ P₂
inst✝ : TopologicalSpace P₂
⊢ Injective toAffineEquiv

Tactic:
intro e e' H

Result:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module k V₁
inst✝⁵ : AddTorsor V₁ P₁
inst✝⁴ : TopologicalSpace P₁
inst✝³ : AddCommGroup V₂
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₂ P₂
inst✝ : TopologicalSpace P₂
e e' : P₁ ≃ᵃL[k] P₂
H : ↑e = ↑e'
⊢ e = e'

Proof state:
case mk
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module k V₁
inst✝⁵ : AddTorsor V₁ P₁
inst✝⁴ : TopologicalSpace P₁
inst✝³ : AddCommGroup V₂
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₂ P₂
inst✝ : TopologicalSpace P₂
e' : P₁ ≃ᵃL[k] P₂
toAffineEquiv✝ : P₁ ≃ᵃ[k] P₂
continuous_toFun✝ : Continuous toAffineEquiv✝.toFun
continuous_invFun✝ : Continuous toAffineEquiv✝.invFun
H :
  ↑{ toAffineEquiv := toAffineEquiv✝, continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ } =
    ↑e'
⊢ { toAffineEquiv := toAffineEquiv✝, continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ } =
    e'

Tactic:
congr

Result:
no goals

Proof state:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module k V₁
inst✝⁵ : AddTorsor V₁ P₁
inst✝⁴ : TopologicalSpace P₁
inst✝³ : AddCommGroup V₂
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₂ P₂
inst✝ : TopologicalSpace P₂
e e' : P₁ ≃ᵃL[k] P₂
H : ↑e = ↑e'
⊢ e = e'

Tactic:
cases e

Result:
case mk
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module k V₁
inst✝⁵ : AddTorsor V₁ P₁
inst✝⁴ : TopologicalSpace P₁
inst✝³ : AddCommGroup V₂
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₂ P₂
inst✝ : TopologicalSpace P₂
e' : P₁ ≃ᵃL[k] P₂
toAffineEquiv✝ : P₁ ≃ᵃ[k] P₂
continuous_toFun✝ : Continuous toAffineEquiv✝.toFun
continuous_invFun✝ : Continuous toAffineEquiv✝.invFun
H :
  ↑{ toAffineEquiv := toAffineEquiv✝, continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ } =
    ↑e'
⊢ { toAffineEquiv := toAffineEquiv✝, continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ } =
    e'